1  /-
  2  Copyright (c) 2017 Johannes Hölzl. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot
  5  -/
  6  import topology.maps
src         └───────────┘
  7  
  8  /-!
  9  # Constructions of new topological spaces from old ones
 10  
 11  This file constructs products, sums, subtypes and quotients of topological spaces
 12  and sets up their basic theory, such as criteria for maps into or out of these
 13  constructions to be continuous; descriptions of the open sets, neighborhood filters,
 14  and generators of these constructions; and their behavior with respect to embeddings
 15  and other specific classes of maps.
 16  
 17  ## Implementation note
 18  
 19  The constructed topologies are defined using induced and coinduced topologies
 20  along with the complete lattice structure on topologies. Their universal properties
 21  (for example, a map `X → Y × Z` is continuous if and only if both projections
 22  `X → Y`, `X → Z` are) follow easily using order-theoretic descriptions of
 23  continuity. With more work we can also extract descriptions of the open sets,
 24  neighborhood filters and so on.
 25  
 26  ## Tags
 27  
 28  product, sum, disjoint union, subspace, quotient space
 29  
 30  -/
 31  
 32  noncomputable theory
 33  
 34  open topological_space set filter lattice
 35  open_locale classical topological_space
 36  
 37  universes u v w x
 38  variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x}
 39  
 40  section constructions
 41  
 42  instance {p : α → Prop} [t : topological_space α] : topological_space (subtype p) :=
id                               └───────────────┘     └───────────────┘  └─────┘ 
src                               └───────────────┘      └───────────────┘  └─────┘
typ                              └───────────────┘     └───────────────┘  └─────┘ 
doc                               └───────────────┘      └───────────────┘
 43  induced subtype.val t
id   └─────┘ └─────────┘ 
src  └─────┘ └─────────┘
typ  └─────┘ └─────────┘ 
doc  └─────┘
 44  
 45  instance {r : α → α → Prop} [t : topological_space α] : topological_space (quot r) :=
id                                  └───────────────┘     └───────────────┘  └──┘ 
src                                   └───────────────┘      └───────────────┘
typ                                 └───────────────┘     └───────────────┘  └──┘ 
doc                                   └───────────────┘      └───────────────┘
 46  coinduced (quot.mk r) t
id   └───────┘  └─────┘   
src  └───────┘
typ  └───────┘  └─────┘   
doc  └───────┘
 47  
 48  instance {s : setoid α} [t : topological_space α] : topological_space (quotient s) :=
id                 └────┘        └───────────────┘     └───────────────┘  └──────┘ 
src                └────┘         └───────────────┘      └───────────────┘  └──────┘
typ                └────┘        └───────────────┘     └───────────────┘  └──────┘ 
doc                               └───────────────┘      └───────────────┘
 49  coinduced quotient.mk t
id   └───────┘ └─────────┘ 
src  └───────┘ └─────────┘
typ  └───────┘ └─────────┘ 
doc  └───────┘
 50  
 51  instance [t₁ : topological_space α] [t₂ : topological_space β] : topological_space (α × β) :=
id                  └───────────────┘         └───────────────┘     └───────────────┘    
src                 └───────────────┘          └───────────────┘      └───────────────┘    
typ                 └───────────────┘         └───────────────┘     └───────────────┘    
doc                 └───────────────┘          └───────────────┘      └───────────────┘
 52  induced prod.fst t₁ ⊓ induced prod.snd t₂
id   └─────┘ └──────┘ └┘  └─────┘ └──────┘ └┘
src  └─────┘ └──────┘     └─────┘ └──────┘
typ  └─────┘ └──────┘ └┘  └─────┘ └──────┘ └┘
doc  └─────┘               └─────┘
 53  
 54  instance [t₁ : topological_space α] [t₂ : topological_space β] : topological_space (α ⊕ β) :=
id                  └───────────────┘         └───────────────┘     └───────────────┘    
src                 └───────────────┘          └───────────────┘      └───────────────┘    
typ                 └───────────────┘         └───────────────┘     └───────────────┘    
doc                 └───────────────┘          └───────────────┘      └───────────────┘
 55  coinduced sum.inl t₁ ⊔ coinduced sum.inr t₂
id   └───────┘ └─────┘ └┘  └───────┘ └─────┘ └┘
src  └───────┘ └─────┘     └───────┘ └─────┘
typ  └───────┘ └─────┘ └┘  └───────┘ └─────┘ └┘
doc  └───────┘              └───────┘
 56  
 57  instance {β : α → Type v} [t₂ : Πa, topological_space (β a)] : topological_space (sigma β) :=
id                                     └───────────────┘        └───────────────┘  └───┘ 
src                                      └───────────────┘          └───────────────┘  └───┘
typ                                    └───────────────┘        └───────────────┘  └───┘ 
doc                                      └───────────────┘          └───────────────┘
 58  ⨆a, coinduced (sigma.mk a) (t₂ a)
id    └───────┘  └──────┘    └┘ 
src    └───────┘  └──────┘
typ   └───────┘  └──────┘    └┘ 
doc    └───────┘
 59  
 60  instance Pi.topological_space {β : α → Type v} [t₂ : Πa, topological_space (β a)] :
id                                                          └───────────────┘   
src                                                           └───────────────┘
typ                                                         └───────────────┘   
doc                                                           └───────────────┘
 61    topological_space (Πa, β a) :=
id     └───────────────┘      
src    └───────────────┘
typ    └───────────────┘      
doc    └───────────────┘
 62  ⨅a, induced (λf, f a) (t₂ a)
id    └─────┘         └┘ 
src    └─────┘
typ   └─────┘         └┘ 
doc    └─────┘
 63  
 64  lemma quotient_dense_of_dense [setoid α] [topological_space α] {s : set α} (H : ∀ x, x ∈ closure s) :
id                                  └────┘    └───────────────┘        └─┘              └─────┘ 
src                                 └────┘     └───────────────┘         └─┘                 └─────┘
typ                                 └────┘    └───────────────┘        └─┘              └─────┘ 
doc                                            └───────────────┘                              └─────┘
 65    closure (quotient.mk '' s) = univ :=
id     └─────┘  └─────────┘ └┘    └──┘
src    └─────┘  └─────────┘ └┘     └──┘
typ    └─────┘  └─────────┘ └┘    └──┘
doc    └─────┘
 66  eq_univ_of_forall $ λ x, begin
id   └───────────────┘     
src  └───────────────┘
typ  └───────────────┘     
st                            └─────
 67    rw mem_closure_iff,
id        └─────────────┘
src    └─┘└─────────────┘
typ    └─┘└─────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ───────────────────┘└─
 68    intros U U_op x_in_U,
src    └──────────────────┘
typ    └──────────────────┘
doc    └──────────────────┘
txt    └──────────────────┘
par    └──────────────────┘
pid          └────────────┘
st   ─────────────────────┘└─
 69    let V := quotient.mk ⁻¹' U,
id              └─────────┘ └─┘ 
src    └───────┘└─────────┘└─┘
typ    └───────┘└─────────┘└─┘
doc    └───────┘           └─┘
txt    └───────┘              
par    └───────┘              
pid    └───┘└─┘              
st   ───────────────────────────┘└─
 70    cases quotient.exists_rep x with y y_x,
id           └─────────────────┘ 
src    └────┘└─────────────────┘ └─────────┘
typ    └────┘└─────────────────┘└─────────┘
doc    └────┘                    └─────────┘
txt    └────┘                    └─────────┘
par    └────┘                    └─────────┘
pid                             └─────────┘
st   ───────────────────────────────────────┘└─
 71    have y_in_V : y ∈ V, by simp only [mem_preimage, y_x, x_in_U],
id                                     └──────────┘  └─┘  └────┘
src    └────────────┘       └─────────┘└──────────┘└┘   └┘      
typ    └────────────┘     └─────────┘└──────────┘└┘└─┘└┘└────┘
doc    └────────────┘        └─────────┘            └┘   └┘      
txt    └────────────┘        └─────────┘            └┘   └┘      
par    └────────────┘        └─────────┘            └┘   └┘      
pid    └─────────┘└─┘            └──┘└┘            └┘   └┘      
st   ────────────────────┘                                          └─
 72    have V_op : is_open V := U_op,
id                 └─────┘     └──┘
src    └──────────┘└─────┘ └──┘
typ    └──────────┘└─────┘└──┘└──┘
doc    └──────────┘└─────┘ └──┘
txt    └──────────┘        └──┘
par    └──────────┘        └──┘
pid    └───────┘└─┘        └──┘
st   ──────────────────────────────┘└─
 73    obtain ⟨w, w_in_V, w_in_range⟩ : (V ∩ s).nonempty := mem_closure_iff.1 (H y) V V_op y_in_V,
id                                                        └─────────────┘        └──┘ └────┘
src    └───────────────────────────────┘   └────────────┘└─────────────┘└─┘   └┘     
typ    └───────────────────────────────┘  └────────────┘└─────────────┘└─┘ └┘└──┘└────┘
doc    └───────────────────────────────┘    └────────────┘               └─┘   └┘     
txt    └───────────────────────────────┘    └────────────┘               └─┘   └┘     
par    └───────────────────────────────┘    └────────────┘               └─┘   └┘     
pid          └─────────────────────────┘    └────────────┘               └─┘   └┘     
st   ───────────────────────────────────────────────────────────────────────────────────────────┘└─
 74    exact ⟨_, w_in_V, mem_image_of_mem quotient.mk w_in_range⟩
id               └────┘  └──────────────┘ └─────────┘ └────────┘
src    └────┘ └─┘      └┘└──────────────┘└─────────┘          └┘
typ    └────┘ └─┘└────┘└┘└──────────────┘└─────────┘└────────┘└┘
doc    └────┘ └─┘      └┘                                     └┘
txt    └────┘ └─┘      └┘                                     └┘
par    └────┘ └─┘      └┘                                     └┘
pid          └─┘      └┘                                     
st   ────────────────────────────────────────────────────────────┘
 75  end
st   └─┘
 76  
 77  instance {p : α → Prop} [topological_space α] [discrete_topology α] :
id                           └───────────────┘    └───────────────┘ 
src                           └───────────────┘     └───────────────┘
typ                          └───────────────┘    └───────────────┘ 
doc                           └───────────────┘     └───────────────┘
 78    discrete_topology (subtype p) :=
id     └───────────────┘  └─────┘ 
src    └───────────────┘  └─────┘
typ    └───────────────┘  └─────┘ 
doc    └───────────────┘
 79  ⟨bot_unique $ assume s hs,
id    └────────┘           └┘
src   └────────┘
typ   └────────┘           └┘
 80    ⟨subtype.val '' s, is_open_discrete _, (set.preimage_image_eq _ subtype.val_injective)⟩⟩
id      └─────────┘ └┘   └──────────────┘     └───────────────────┘   └───────────────────┘
src     └─────────┘ └┘    └──────────────┘     └───────────────────┘   └───────────────────┘
typ     └─────────┘ └┘   └──────────────┘     └───────────────────┘   └───────────────────┘
 81  
 82  instance sum.discrete_topology [topological_space α] [topological_space β]
id                                   └───────────────┘    └───────────────┘ 
src                                  └───────────────┘     └───────────────┘
typ                                  └───────────────┘    └───────────────┘ 
doc                                  └───────────────┘     └───────────────┘
 83    [hα : discrete_topology α] [hβ : discrete_topology β] : discrete_topology (α ⊕ β) :=
id           └───────────────┘         └───────────────┘     └───────────────┘    
src          └───────────────┘          └───────────────┘      └───────────────┘    
typ          └───────────────┘         └───────────────┘     └───────────────┘    
doc          └───────────────┘          └───────────────┘      └───────────────┘
 84  ⟨by unfold sum.topological_space; simp [hα.eq_bot, hβ.eq_bot]⟩
src      └──────────────────────────┘  └────┘         └┘         
typ      └──────────────────────────┘  └────┘└───────┘└┘└───────┘
doc      └──────────────────────────┘  └────┘         └┘         
txt      └──────────────────────────┘  └────┘         └┘         
par      └──────────────────────────┘  └────┘         └┘         
pid            └────────────────────┘               └┘         
st      └────────────────────────────────────────────────────────┘
 85  
 86  instance sigma.discrete_topology {β : α → Type v} [Πa, topological_space (β a)]
id                                                        └───────────────┘   
src                                                         └───────────────┘
typ                                                       └───────────────┘   
doc                                                         └───────────────┘
 87    [h : Πa, discrete_topology (β a)] : discrete_topology (sigma β) :=
id             └───────────────┘        └───────────────┘  └───┘ 
src             └───────────────┘          └───────────────┘  └───┘
typ            └───────────────┘        └───────────────┘  └───┘ 
doc             └───────────────┘          └───────────────┘
 88  ⟨by { unfold sigma.topological_space, simp [λ a, (h a).eq_bot] }⟩
id                                                     
src        └────────────────────────────┘  └────┘ └──┘   └────────┘
typ        └────────────────────────────┘  └────┘ └──┘  └────────┘
doc        └────────────────────────────┘  └────┘ └──┘   └────────┘
txt        └────────────────────────────┘  └────┘ └──┘   └────────┘
par        └────────────────────────────┘  └────┘ └──┘   └────────┘
pid              └──────────────────────┘       └──┘   └───────┘
st      └───────────────────────────────┘└─────────────────────────┘└┘
 89  
 90  section topα
 91  
 92  variable [topological_space α]
id             └───────────────┘
src            └───────────────┘
typ            └───────────────┘
doc            └───────────────┘
 93  
 94  /-
 95  The 𝓝 filter and the subspace topology.
 96  -/
 97  
 98  theorem mem_nhds_subtype (s : set α) (a : {x // x ∈ s}) (t : set {x // x ∈ s}) :
id                                 └─┘                      └─┘       
src                                └─┘                          └─┘        
typ                                └─┘                      └─┘       
 99    t ∈ 𝓝 a ↔ ∃ u ∈ 𝓝 a.val, (@subtype.val α s) ⁻¹' u ⊆ t :=
id               └──┘   └─────────┘    └─┘   
src                  └──┘   └─────────┘      └─┘   
typ              └──┘   └─────────┘    └─┘   
doc                                              └─┘
100  mem_nhds_induced subtype.val a t
id   └──────────────┘ └─────────┘  
src  └──────────────┘ └─────────┘
typ  └──────────────┘ └─────────┘  
101  
102  theorem nhds_subtype (s : set α) (a : {x // x ∈ s}) :
id                             └─┘              
src                            └─┘                
typ                            └─┘              
103    𝓝 a = comap subtype.val (𝓝 a.val) :=
id        └───┘ └─────────┘   └──┘
src        └───┘ └─────────┘    └──┘
typ       └───┘ └─────────┘   └──┘
doc         └───┘              
104  nhds_induced subtype.val a
id   └──────────┘ └─────────┘ 
src  └──────────┘ └─────────┘
typ  └──────────┘ └─────────┘ 
105  
106  end topα
107  
108  end constructions
109  
110  
111  section prod
112  open topological_space
113  variables [topological_space α] [topological_space β] [topological_space γ] [topological_space δ]
id              └───────────────┘     └───────────────┘     └───────────────┘     └───────────────┘
src             └───────────────┘     └───────────────┘     └───────────────┘     └───────────────┘
typ             └───────────────┘     └───────────────┘     └───────────────┘     └───────────────┘
doc             └───────────────┘     └───────────────┘     └───────────────┘     └───────────────┘
114  
115  lemma continuous_fst : continuous (@prod.fst α β) :=
id                          └────────┘   └──────┘  
src                         └────────┘   └──────┘
typ                         └────────┘   └──────┘  
doc                         └────────┘
116  continuous_inf_dom_left continuous_induced_dom
id   └─────────────────────┘ └────────────────────┘
src  └─────────────────────┘ └────────────────────┘
typ  └─────────────────────┘ └────────────────────┘
117  
118  lemma continuous_snd : continuous (@prod.snd α β) :=
id                          └────────┘   └──────┘  
src                         └────────┘   └──────┘
typ                         └────────┘   └──────┘  
doc                         └────────┘
119  continuous_inf_dom_right continuous_induced_dom
id   └──────────────────────┘ └────────────────────┘
src  └──────────────────────┘ └────────────────────┘
typ  └──────────────────────┘ └────────────────────┘
120  
121  lemma continuous.prod_mk {f : γ → α} {g : γ → β}
id                                              
typ                                             
122    (hf : continuous f) (hg : continuous g) : continuous (λx, prod.mk (f x) (g x)) :=
id           └────────┘         └────────┘     └────────┘     └─────┘       
src          └────────┘          └────────┘      └────────┘      └─────┘
typ          └────────┘         └────────┘     └────────┘     └─────┘       
doc          └────────┘          └────────┘      └────────┘
123  continuous_inf_rng (continuous_induced_rng hf) (continuous_induced_rng hg)
id   └────────────────┘  └────────────────────┘ └┘   └────────────────────┘ └┘
src  └────────────────┘  └────────────────────┘      └────────────────────┘
typ  └────────────────┘  └────────────────────┘ └┘   └────────────────────┘ └┘
124  
125  lemma continuous_swap : continuous (prod.swap : α × β → β × α) :=
id                           └────────┘  └───────┘          
src                          └────────┘  └───────┘            
typ                          └────────┘  └───────┘          
doc                          └────────┘  └───────┘
126  continuous.prod_mk continuous_snd continuous_fst
id   └────────────────┘ └────────────┘ └────────────┘
src  └────────────────┘ └────────────┘ └────────────┘
typ  └────────────────┘ └────────────┘ └────────────┘
127  
128  lemma is_open_prod {s : set α} {t : set β} (hs : is_open s) (ht : is_open t) :
id                           └─┘        └─┘         └─────┘         └─────┘ 
src                          └─┘         └─┘          └─────┘          └─────┘
typ                          └─┘        └─┘         └─────┘         └─────┘ 
doc                                                   └─────┘          └─────┘
129    is_open (set.prod s t) :=
id     └─────┘  └──────┘  
src    └─────┘  └──────┘
typ    └─────┘  └──────┘  
doc    └─────┘  └──────┘
130  is_open_inter (continuous_fst s hs) (continuous_snd t ht)
id   └───────────┘  └────────────┘  └┘   └────────────┘  └┘
src  └───────────┘  └────────────┘        └────────────┘
typ  └───────────┘  └────────────┘  └┘   └────────────┘  └┘
131  
132  lemma nhds_prod_eq {a : α} {b : β} : 𝓝 (a, b) = filter.prod (𝓝 a) (𝓝 b) :=
id                                            └─────────┘       
src                                               └─────────┘       
typ                                           └─────────┘       
doc                                                 └─────────┘       
133  by rw [filter.prod, prod.topological_space, nhds_inf, nhds_induced, nhds_induced]
id          └─────────┘  └────────────────────┘  └──────┘  └──────────┘  └──────────┘
src     └──┘└─────────┘└┘└────────────────────┘└┘└──────┘└┘└──────────┘└┘└──────────┘└─
typ     └──┘└─────────┘└┘└────────────────────┘└┘└──────┘└┘└──────────┘└┘└──────────┘└─
doc     └──┘└─────────┘└┘                      └┘        └┘            └┘            └─
txt     └──┘           └┘                      └┘        └┘            └┘            └─
par     └──┘           └┘                      └┘        └┘            └┘            └─
pid       └┘           └┘                      └┘        └┘            └┘            
st     └──────────────┘└──────────────────────┘└────────┘└────────────┘└────────────┘
134  
src  
typ  
doc  
txt  
par  
pid  
st   
135  instance [discrete_topology α] [discrete_topology β] : discrete_topology (α × β) :=
id             └───────────────┘    └───────────────┘     └───────────────┘    
src            └───────────────┘     └───────────────┘      └───────────────┘    
typ            └───────────────┘    └───────────────┘     └───────────────┘    
doc            └───────────────┘     └───────────────┘      └───────────────┘
136  ⟨eq_of_nhds_eq_nhds $ assume ⟨a, b⟩,
id    └────────────────┘          
src   └────────────────┘
typ   └────────────────┘          
137    by rw [nhds_prod_eq, nhds_discrete α, nhds_discrete β, nhds_bot, filter.prod_pure_pure]⟩
id            └──────────┘  └───────────┘   └───────────┘   └──────┘  └───────────────────┘
src       └──┘└──────────┘└┘└───────────┘ └┘└───────────┘ └┘└──────┘└┘└───────────────────┘
typ       └──┘└──────────┘└┘└───────────┘└┘└───────────┘└┘└──────┘└┘└───────────────────┘
doc       └──┘            └┘              └┘              └┘        └┘                     
txt       └──┘            └┘              └┘              └┘        └┘                     
par       └──┘            └┘              └┘              └┘        └┘                     
pid         └┘            └┘              └┘              └┘        └┘                     
st       └───────────────┘└───────────────┘└───────────────┘└────────┘└─────────────────────┘
138  
139  lemma prod_mem_nhds_sets {s : set α} {t : set β} {a : α} {b : β}
id                                 └─┘        └─┘               
src                                └─┘         └─┘
typ                                └─┘        └─┘               
140    (ha : s ∈ 𝓝 a) (hb : t ∈ 𝓝 b) : set.prod s t ∈ 𝓝 (a, b) :=
id                             └──────┘       
src                                └──────┘       
typ                            └──────┘       
doc                                  └──────┘       
141  by rw [nhds_prod_eq]; exact prod_mem_prod ha hb
id          └──────────┘         └───────────┘ └┘ └┘
src     └──┘└──────────┘  └────┘└───────────┘    
typ     └──┘└──────────┘  └────┘└───────────┘└┘└┘
doc     └──┘              └────┘                 
txt     └──┘              └────┘                 
par     └──┘              └────┘                 
pid       └┘                                    
st     └───────────────┘└───────────────────────────
142  
src  
typ  
doc  
txt  
par  
pid  
st   
143  lemma nhds_swap (a : α) (b : β) : 𝓝 (a, b) = (𝓝 (b, a)).map prod.swap :=
id                                               └─┘  └───────┘
src                                                    └─┘  └───────┘
typ                                              └─┘  └───────┘
doc                                                       └─┘  └───────┘
144  by rw [nhds_prod_eq, filter.prod_comm, nhds_prod_eq]; refl
id          └──────────┘  └──────────────┘  └──────────┘
src     └──┘└──────────┘└┘└──────────────┘└┘└──────────┘  └────
typ     └──┘└──────────┘└┘└──────────────┘└┘└──────────┘  └────
doc     └──┘            └┘                └┘              └────
txt     └──┘            └┘                └┘              └────
par     └──┘            └┘                └┘              └────
pid       └┘            └┘                └┘                  
st     └───────────────┘└────────────────┘└────────────┘└──────
145  
src  
typ  
doc  
txt  
par  
pid  
st   
146  lemma tendsto_prod_mk_nhds {γ} {a : α} {b : β} {f : filter γ} {ma : γ → α} {mb : γ → β}
id                                                     └────┘                       
src                                                      └────┘
typ                                                    └────┘                       
147    (ha : tendsto ma f (𝓝 a)) (hb : tendsto mb f (𝓝 b)) :
id           └─────┘ └┘             └─────┘ └┘    
src          └─────┘                  └─────┘       
typ          └─────┘ └┘             └─────┘ └┘    
doc          └─────┘                  └─────┘       
148    tendsto (λc, (ma c, mb c)) f (𝓝 (a, b)) :=
id     └─────┘     └┘   └┘         
src    └─────┘                       
typ    └─────┘     └┘   └┘         
doc    └─────┘                       
149  by rw [nhds_prod_eq]; exact filter.tendsto.prod_mk ha hb
id          └──────────┘         └────────────────────┘ └┘ └┘
src     └──┘└──────────┘  └────┘└────────────────────┘    
typ     └──┘└──────────┘  └────┘└────────────────────┘└┘└┘
doc     └──┘              └────┘                          
txt     └──┘              └────┘                          
par     └──┘              └────┘                          
pid       └┘                                             
st     └───────────────┘└────────────────────────────────────
150  
src  
typ  
doc  
txt  
par  
pid  
st   
151  lemma continuous_at.prod {f : α → β} {g : α → γ} {x : α}
id                                                     
typ                                                    
152    (hf : continuous_at f x) (hg : continuous_at g x) : continuous_at (λx, (f x, g x)) x :=
id           └───────────┘          └───────────┘      └───────────┘            
src          └───────────┘            └───────────┘        └───────────┘      
typ          └───────────┘          └───────────┘      └───────────┘            
doc          └───────────┘            └───────────┘        └───────────┘
153  tendsto_prod_mk_nhds hf hg
id   └──────────────────┘ └┘ └┘
src  └──────────────────┘
typ  └──────────────────┘ └┘ └┘
154  
155  lemma prod_generate_from_generate_from_eq {α : Type*} {β : Type*} {s : set (set α)} {t : set (set β)}
id                                                                          └─┘  └─┘         └─┘  └─┘ 
src                                                                         └─┘  └─┘          └─┘  └─┘
typ                                                                         └─┘  └─┘         └─┘  └─┘ 
156    (hs : ⋃₀ s = univ) (ht : ⋃₀ t = univ) :
id           └┘   └──┘        └┘   └──┘
src          └┘    └──┘        └┘    └──┘
typ          └┘   └──┘        └┘   └──┘
157    @prod.topological_space α β (generate_from s) (generate_from t) =
id      └────────────────────┘    └───────────┘    └───────────┘   
src     └────────────────────┘      └───────────┘     └───────────┘    
typ     └────────────────────┘    └───────────┘    └───────────┘   
doc                                 └───────────┘     └───────────┘
158    generate_from {g | ∃u∈s, ∃v∈t, g = set.prod u v} :=
id     └───────────┘          └──────┘  
src    └───────────┘                └──────┘
typ    └───────────┘          └──────┘  
doc    └───────────┘                      └──────┘
159  let G := generate_from {g | ∃u∈s, ∃v∈t, g = set.prod u v} in
id           └───────────┘          └──────┘  
src           └───────────┘                └──────┘
typ          └───────────┘          └──────┘  
doc           └───────────┘                      └──────┘
160  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
161    (le_generate_from $ assume g ⟨u, hu, v, hv, g_eq⟩, g_eq.symm ▸
id      └──────────────┘              └┘     └┘  └──┘       └───┘ 
src     └──────────────┘                                      └───┘ 
typ     └──────────────┘              └┘     └┘  └──┘       └───┘ 
162      @is_open_prod _ _ (generate_from s) (generate_from t) _ _
id        └──────────┘      └───────────┘    └───────────┘ 
src       └──────────┘      └───────────┘     └───────────┘
typ       └──────────┘      └───────────┘    └───────────┘ 
doc                         └───────────┘     └───────────┘
163        (generate_open.basic _ hu) (generate_open.basic _ hv))
id          └─────────────────┘        └─────────────────┘
src         └─────────────────┘        └─────────────────┘
typ         └─────────────────┘        └─────────────────┘
164    (le_inf
id      └────┘
src     └────┘
typ     └────┘
165      (coinduced_le_iff_le_induced.mp $ le_generate_from $ assume u hu,
id        └─────────────────────────┘└─┘   └──────────────┘           └┘
src       └─────────────────────────┘└─┘   └──────────────┘
typ       └─────────────────────────┘└─┘   └──────────────┘           └┘
166        have (⋃v∈t, set.prod u v) = prod.fst ⁻¹' u,
id                 └──────┘     └──────┘ └─┘ 
src                  └──────┘       └──────┘ └─┘
typ                └──────┘     └──────┘ └─┘ 
doc                  └──────┘                 └─┘
167          from calc (⋃v∈t, set.prod u v) = set.prod u univ :
id                        └──────┘      └──────┘  └──┘
src                         └──────┘        └──────┘   └──┘
typ                       └──────┘      └──────┘  └──┘
doc                         └──────┘        └──────┘
168              set.ext $ assume ⟨a, b⟩, by rw ← ht; simp [and.left_comm] {contextual:=tt}
id               └─────┘                         └┘        └───────────┘               └┘
src              └─────┘                     └───┘    └────┘└───────────┘└┘ └──────────┘└┘└─
typ              └─────┘                    └───┘└┘  └────┘└───────────┘└┘ └──────────┘└┘└─
doc                                          └───┘    └────┘             └┘ └──────────┘  └─
txt                                          └───┘    └────┘             └┘ └──────────┘  └─
par                                          └───┘    └────┘             └┘ └──────────┘  └─
pid                                            └─┘                      └──────────┘  
st                                          └───────────────────────────────────────────────
169            ... = prod.fst ⁻¹' u : by simp [set.prod, preimage],
id                   └──────┘ └─┘             └──────┘  └──────┘
src  ─────────┘      └──────┘ └─┘        └────┘└──────┘└┘└──────┘
typ  ─────────┘      └──────┘ └─┘       └────┘└──────┘└┘└──────┘
doc  ─────────┘               └─┘        └────┘└──────┘└┘└──────┘
txt  ─────────┘                          └────┘        └┘        
par  ─────────┘                          └────┘        └┘        
pid  ─────────┘                                      └┘        
st   ─────────┘                         └────────────────────────┘
170        show G.is_open (prod.fst ⁻¹' u),
id              └──────┘  └──────┘ └─┘ 
src              └──────┘  └──────┘ └─┘
typ             └──────┘  └──────┘ └─┘ 
doc                                 └─┘
171          from this ▸ @is_open_Union _ _ G _ $ assume v, @is_open_Union _ _ G _ $ assume hv,
id                └──┘   └───────────┘                    └───────────┘                 └┘
src                      └───────────┘                      └───────────┘
typ               └──┘   └───────────┘                    └───────────┘                 └┘
172            generate_open.basic _ ⟨_, hu, _, hv, rfl⟩)
id             └─────────────────┘       └┘     └┘  └─┘
src            └─────────────────┘                  └─┘
typ            └─────────────────┘       └┘     └┘  └─┘
173      (coinduced_le_iff_le_induced.mp $ le_generate_from $ assume v hv,
id        └─────────────────────────┘└─┘   └──────────────┘           └┘
src       └─────────────────────────┘└─┘   └──────────────┘
typ       └─────────────────────────┘└─┘   └──────────────┘           └┘
174        have (⋃u∈s, set.prod u v) = prod.snd ⁻¹' v,
id                 └──────┘     └──────┘ └─┘ 
src                  └──────┘       └──────┘ └─┘
typ                └──────┘     └──────┘ └─┘ 
doc                  └──────┘                 └─┘
175          from calc (⋃u∈s, set.prod u v) = set.prod univ v:
id                        └──────┘      └──────┘ └──┘ 
src                         └──────┘        └──────┘ └──┘
typ                       └──────┘      └──────┘ └──┘ 
doc                         └──────┘        └──────┘
176              set.ext $ assume ⟨a, b⟩, by rw [←hs]; by_cases b ∈ v; simp [h] {contextual:=tt}
id               └─────┘                         └┘                                     └┘
src              └─────┘                     └───┘    └───────┘    └────┘ └┘ └──────────┘└┘└─
typ              └─────┘                    └───┘└┘  └───────┘  └────┘└┘ └──────────┘└┘└─
doc                                          └───┘    └───────┘     └────┘ └┘ └──────────┘  └─
txt                                          └───┘    └───────┘     └────┘ └┘ └──────────┘  └─
par                                          └───┘    └───────┘     └────┘ └┘ └──────────┘  └─
pid                                            └─┘                       └──────────┘  
st                                          └──────┘└───────────────────────────────────────────
177            ... = prod.snd ⁻¹' v : by simp [set.prod, preimage],
id                   └──────┘ └─┘             └──────┘  └──────┘
src  ─────────┘      └──────┘ └─┘        └────┘└──────┘└┘└──────┘
typ  ─────────┘      └──────┘ └─┘       └────┘└──────┘└┘└──────┘
doc  ─────────┘               └─┘        └────┘└──────┘└┘└──────┘
txt  ─────────┘                          └────┘        └┘        
par  ─────────┘                          └────┘        └┘        
pid  ─────────┘                                      └┘        
st   ─────────┘                         └────────────────────────┘
178        show G.is_open (prod.snd ⁻¹' v),
id              └──────┘  └──────┘ └─┘ 
src              └──────┘  └──────┘ └─┘
typ             └──────┘  └──────┘ └─┘ 
doc                                 └─┘
179          from this ▸ @is_open_Union _ _ G _ $ assume u, @is_open_Union _ _ G _ $ assume hu,
id                └──┘   └───────────┘                    └───────────┘                 └┘
src                      └───────────┘                      └───────────┘
typ               └──┘   └───────────┘                    └───────────┘                 └┘
180            generate_open.basic _ ⟨_, hu, _, hv, rfl⟩))
id             └─────────────────┘       └┘     └┘  └─┘
src            └─────────────────┘                  └─┘
typ            └─────────────────┘       └┘     └┘  └─┘
181  
182  lemma prod_eq_generate_from :
183    prod.topological_space =
id     └────────────────────┘ 
src    └────────────────────┘ 
typ    └────────────────────┘ 
184    generate_from {g | ∃(s:set α) (t:set β), is_open s ∧ is_open t ∧ g = set.prod s t} :=
id     └───────────┘       └─┘      └─┘   └─────┘   └─────┘     └──────┘  
src    └───────────┘        └─┘       └─┘    └─────┘    └─────┘       └──────┘
typ    └───────────┘       └─┘      └─┘   └─────┘   └─────┘     └──────┘  
doc    └───────────┘                            └─────┘     └─────┘         └──────┘
185  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
186    (le_generate_from $ assume g ⟨s, t, hs, ht, g_eq⟩, g_eq.symm ▸ is_open_prod hs ht)
id      └──────────────┘                 └┘  └┘  └──┘       └───┘  └──────────┘
src     └──────────────┘                                      └───┘  └──────────┘
typ     └──────────────┘                 └┘  └┘  └──┘       └───┘  └──────────┘
187    (le_inf
id      └────┘
src     └────┘
typ     └────┘
188      (ball_image_of_ball $ λt ht, generate_open.basic _ ⟨t, univ, by simpa [set.prod_eq] using ht⟩)
id        └────────────────┘     └┘  └─────────────────┘      └──┘            └─────────┘        └┘
src       └────────────────┘          └─────────────────┘       └──┘     └─────┘└─────────┘└──────┘
typ       └────────────────┘     └┘  └─────────────────┘      └──┘     └─────┘└─────────┘└──────┘└┘
doc                                                                      └─────┘           └──────┘
txt                                                                      └─────┘           └──────┘
par                                                                      └─────┘           └──────┘
pid                                                                                      └────┘
st                                                                      └───────────────────────────┘
189      (ball_image_of_ball $ λt ht, generate_open.basic _ ⟨univ, t, by simpa [set.prod_eq] using ht⟩))
id        └────────────────┘     └┘  └─────────────────┘    └──┘              └─────────┘        └┘
src       └────────────────┘          └─────────────────┘    └──┘        └─────┘└─────────┘└──────┘
typ       └────────────────┘     └┘  └─────────────────┘    └──┘       └─────┘└─────────┘└──────┘└┘
doc                                                                      └─────┘           └──────┘
txt                                                                      └─────┘           └──────┘
par                                                                      └─────┘           └──────┘
pid                                                                                      └────┘
st                                                                      └───────────────────────────┘
190  
191  lemma is_open_prod_iff {s : set (α×β)} : is_open s ↔
id                               └─┘       └─────┘  
src                              └─┘         └─────┘   
typ                              └─┘       └─────┘  
doc                                           └─────┘
192    (∀a b, (a, b) ∈ s → ∃u v, is_open u ∧ is_open v ∧ a ∈ u ∧ b ∈ v ∧ set.prod u v ⊆ s) :=
id                    └─────┘   └─────┘           └──────┘    
src                          └─────┘    └─────┘                └──────┘     
typ                   └─────┘   └─────┘           └──────┘    
doc                              └─────┘     └─────┘                     └──────┘
193  begin
st   └─────
194    rw [is_open_iff_nhds],
id         └──────────────┘
src    └──┘└──────────────┘
typ    └──┘└──────────────┘
doc    └──┘                
txt    └──┘                
par    └──┘                
pid      └┘                
st   ─────────────────────┘└──
195    simp [nhds_prod_eq, mem_prod_iff],
id           └──────────┘  └──────────┘
src    └────┘└──────────┘└┘└──────────┘
typ    └────┘└──────────┘└┘└──────────┘
doc    └────┘            └┘            
txt    └────┘            └┘            
par    └────┘            └┘            
pid                    └┘            
st   ──────────────────────────────────┘└─
196    simp [mem_nhds_sets_iff],
id           └───────────────┘
src    └────┘└───────────────┘
typ    └────┘└───────────────┘
doc    └────┘                 
txt    └────┘                 
par    └────┘                 
pid                         
st   ─────────────────────────┘└─
197    exact forall_congr (assume a, ball_congr $ assume b h,
id           └──────────┘            └────────┘
src    └────┘└──────────┘       └──┘└────────┘       └─────
typ    └────┘└──────────┘       └──┘└────────┘       └─────
doc    └────┘                   └──┘                 └─────
txt    └────┘                   └──┘                 └─────
par    └────┘                   └──┘                 └─────
pid                            └──┘                 └─────
st   ─────────────────────────────────────────────────────────
198      ⟨assume ⟨u', ⟨u, us, uo, au⟩, v', ⟨v, vs, vo, bv⟩, h⟩,
id                       └┘  └┘  └┘          └┘  └┘  └┘   
src  ───┘       └┘  └┘  └┘  └┘  └┘  └─┘  └┘  └┘  └┘  └┘  └─┘ └──
typ  ───┘       └┘  └┘ └┘└┘└┘└┘└┘└┘└─┘  └┘ └┘└┘└┘└┘└┘└┘└─┘└──
doc  ───┘       └┘  └┘  └┘  └┘  └┘  └─┘  └┘  └┘  └┘  └┘  └─┘ └──
txt  ───┘       └┘  └┘  └┘  └┘  └┘  └─┘  └┘  └┘  └┘  └┘  └─┘ └──
par  ───┘       └┘  └┘  └┘  └┘  └┘  └─┘  └┘  └┘  └┘  └┘  └─┘ └──
pid  ───┘       └┘  └┘  └┘  └┘  └┘  └─┘  └┘  └┘  └┘  └┘  └─┘ └──
st   ───────────────────────────────────────────────────────────
199        ⟨u, uo, v, vo, au, bv, subset.trans (set.prod_mono us vs) h⟩,
id                                └──────────┘  └───────────┘
src  ─────┘  └┘  └┘ └┘  └┘  └┘  └┘└──────────┘ └───────────┘    └┘ └──
typ  ─────┘  └┘  └┘ └┘  └┘  └┘  └┘└──────────┘ └───────────┘    └┘ └──
doc  ─────┘  └┘  └┘ └┘  └┘  └┘  └┘                              └┘ └──
txt  ─────┘  └┘  └┘ └┘  └┘  └┘  └┘                              └┘ └──
par  ─────┘  └┘  └┘ └┘  └┘  └┘  └┘                              └┘ └──
pid  ─────┘  └┘  └┘ └┘  └┘  └┘  └┘                              └┘ └──
st   ────────────────────────────────────────────────────────────────────
200        assume ⟨u, uo, v, vo, au, bv, h⟩,
id                   └┘    └┘  └┘  └┘  
src  ─────┘      └┘ └┘  └┘ └┘  └┘  └┘  └┘ └──
typ  ─────┘      └┘└┘└┘└┘└┘└┘└┘└┘└┘└┘└┘└──
doc  ─────┘      └┘ └┘  └┘ └┘  └┘  └┘  └┘ └──
txt  ─────┘      └┘ └┘  └┘ └┘  └┘  └┘  └┘ └──
par  ─────┘      └┘ └┘  └┘ └┘  └┘  └┘  └┘ └──
pid  ─────┘      └┘ └┘  └┘ └┘  └┘  └┘  └┘ └──
st   ────────────────────────────────────────
201        ⟨u, ⟨u, subset.refl u, uo, au⟩, v, ⟨v, subset.refl v, vo, bv⟩, h⟩⟩)
id                                                └─────────┘
src  ─────┘  └┘  └┘            └┘  └┘  └─┘ └┘  └┘└─────────┘ └┘  └┘  └─┘ └──┘
typ  ─────┘  └┘  └┘            └┘  └┘  └─┘ └┘  └┘└─────────┘ └┘  └┘  └─┘ └──┘
doc  ─────┘  └┘  └┘            └┘  └┘  └─┘ └┘  └┘            └┘  └┘  └─┘ └──┘
txt  ─────┘  └┘  └┘            └┘  └┘  └─┘ └┘  └┘            └┘  └┘  └─┘ └──┘
par  ─────┘  └┘  └┘            └┘  └┘  └─┘ └┘  └┘            └┘  └┘  └─┘ └──┘
pid  ─────┘  └┘  └┘            └┘  └┘  └─┘ └┘  └┘            └┘  └┘  └─┘ └─┘
st   ─────────────────────────────────────────────────────────────────────────┘
202  end
st   └─┘
203  
204  /-- The first projection in a product of topological spaces sends open sets to open sets. -/
205  lemma is_open_map_fst : is_open_map (@prod.fst α β) :=
id                           └─────────┘   └──────┘  
src                          └─────────┘   └──────┘
typ                          └─────────┘   └──────┘  
doc                          └─────────┘
206  begin
st   └─────
207    assume s hs,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid    └─────────┘
st   ────────────┘└─
208    rw is_open_iff_forall_mem_open,
id        └─────────────────────────┘
src    └─┘└─────────────────────────┘
typ    └─┘└─────────────────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ───────────────────────────────┘└─
209    assume x xs,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid    └─────────┘
st   ────────────┘└─
210    rw mem_image_eq at xs,
id        └──────────┘
src    └─┘└──────────┘└────┘
typ    └─┘└──────────┘└────┘
doc    └─┘            └────┘
txt    └─┘            └────┘
par    └─┘            └────┘
pid                  └────┘
st   ──────────────────────┘└─
211    rcases xs with ⟨⟨y₁, y₂⟩, ys, yx⟩,
id            └┘
src    └─────┘  └──────────────────────┘
typ    └─────┘└┘└──────────────────────┘
doc    └─────┘  └──────────────────────┘
txt    └─────┘  └──────────────────────┘
par    └─────┘  └──────────────────────┘
pid            └──────────────────────┘
st   ──────────────────────────────────┘└─
212    rcases is_open_prod_iff.1 hs _ _ ys with ⟨o₁, o₂, o₁_open, o₂_open, yo₁, yo₂, ho⟩,
id            └──────────────┘   └┘     └┘
src    └─────┘└──────────────┘└─┘  └───┘  └────────────────────────────────────────────┘
typ    └─────┘└──────────────┘└─┘└┘└───┘└┘└────────────────────────────────────────────┘
doc    └─────┘                └─┘  └───┘  └────────────────────────────────────────────┘
txt    └─────┘                └─┘  └───┘  └────────────────────────────────────────────┘
par    └─────┘                └─┘  └───┘  └────────────────────────────────────────────┘
pid                          └─┘  └───┘  └────────────────────────────────────────────┘
st   ──────────────────────────────────────────────────────────────────────────────────┘└─
213    simp at yx,
src    └────────┘
typ    └────────┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid        └───┘
st   ───────────┘└─
214    rw yx at yo₁,
id        └┘
src    └─┘  └─────┘
typ    └─┘└┘└─────┘
doc    └─┘  └─────┘
txt    └─┘  └─────┘
par    └─┘  └─────┘
pid        └─────┘
st   ─────────────┘└─
215    refine ⟨o₁, _, o₁_open, yo₁⟩,
id             └┘     └─────┘  └─┘
src    └─────┘   └───┘       └┘   
typ    └─────┘ └┘└───┘└─────┘└┘└─┘
doc    └─────┘   └───┘       └┘   
txt    └─────┘   └───┘       └┘   
par    └─────┘   └───┘       └┘   
pid             └───┘       └┘   
st   ─────────────────────────────┘└─
216    assume z zs,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid    └─────────┘
st   ────────────┘└─
217    rw mem_image_eq,
id        └──────────┘
src    └─┘└──────────┘
typ    └─┘└──────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────────────┘└─
218    exact ⟨(z, y₂), ho (by simp [zs, yo₂]), rfl⟩
id               └┘   └┘           └┘  └─┘    └─┘
src    └────┘   └┘  └─┘     └────┘  └┘   └─┘└─┘└┘
typ    └────┘  └┘└┘└─┘└┘   └────┘└┘└┘└─┘└─┘└─┘└┘
doc    └────┘   └┘  └─┘     └────┘  └┘   └─┘   └┘
txt    └────┘   └┘  └─┘     └────┘  └┘   └─┘   └┘
par    └────┘   └┘  └─┘     └────┘  └┘   └─┘   └┘
pid            └┘  └─┘     └─────┘  └┘   └──┘   
st   ───────────────────────┘└─────────────┘└──────┘
219  end
st   └─┘
220  
221  /-- The second projection in a product of topological spaces sends open sets to open sets. -/
222  lemma is_open_map_snd : is_open_map (@prod.snd α β) :=
id                           └─────────┘   └──────┘  
src                          └─────────┘   └──────┘
typ                          └─────────┘   └──────┘  
doc                          └─────────┘
223  begin
st   └─────
224    /- This lemma could be proved by composing the fact that the first projection is open, and
st   ─────────────────────────────────────────────────────────────────────────────────────────────
225    exchanging coordinates is a homeomorphism, hence open. As the `prod_comm` homeomorphism is defined
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────
226    later, we rather go for the direct proof, copy-pasting the proof for the first projection. -/
st   ────────────────────────────────────────────────────────────────────────────────────────────────
227    assume s hs,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid    └─────────┘
st   ────────────┘└─
228    rw is_open_iff_forall_mem_open,
id        └─────────────────────────┘
src    └─┘└─────────────────────────┘
typ    └─┘└─────────────────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ───────────────────────────────┘└─
229    assume x xs,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid    └─────────┘
st   ────────────┘└─
230    rw mem_image_eq at xs,
id        └──────────┘
src    └─┘└──────────┘└────┘
typ    └─┘└──────────┘└────┘
doc    └─┘            └────┘
txt    └─┘            └────┘
par    └─┘            └────┘
pid                  └────┘
st   ──────────────────────┘└─
231    rcases xs with ⟨⟨y₁, y₂⟩, ys, yx⟩,
id            └┘
src    └─────┘  └──────────────────────┘
typ    └─────┘└┘└──────────────────────┘
doc    └─────┘  └──────────────────────┘
txt    └─────┘  └──────────────────────┘
par    └─────┘  └──────────────────────┘
pid            └──────────────────────┘
st   ──────────────────────────────────┘└─
232    rcases is_open_prod_iff.1 hs _ _ ys with ⟨o₁, o₂, o₁_open, o₂_open, yo₁, yo₂, ho⟩,
id            └──────────────┘   └┘     └┘
src    └─────┘└──────────────┘└─┘  └───┘  └────────────────────────────────────────────┘
typ    └─────┘└──────────────┘└─┘└┘└───┘└┘└────────────────────────────────────────────┘
doc    └─────┘                └─┘  └───┘  └────────────────────────────────────────────┘
txt    └─────┘                └─┘  └───┘  └────────────────────────────────────────────┘
par    └─────┘                └─┘  └───┘  └────────────────────────────────────────────┘
pid                          └─┘  └───┘  └────────────────────────────────────────────┘
st   ──────────────────────────────────────────────────────────────────────────────────┘└─
233    simp at yx,
src    └────────┘
typ    └────────┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid        └───┘
st   ───────────┘└─
234    rw yx at yo₂,
id        └┘
src    └─┘  └─────┘
typ    └─┘└┘└─────┘
doc    └─┘  └─────┘
txt    └─┘  └─────┘
par    └─┘  └─────┘
pid        └─────┘
st   ─────────────┘└─
235    refine ⟨o₂, _, o₂_open, yo₂⟩,
id             └┘     └─────┘  └─┘
src    └─────┘   └───┘       └┘   
typ    └─────┘ └┘└───┘└─────┘└┘└─┘
doc    └─────┘   └───┘       └┘   
txt    └─────┘   └───┘       └┘   
par    └─────┘   └───┘       └┘   
pid             └───┘       └┘   
st   ─────────────────────────────┘└─
236    assume z zs,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid    └─────────┘
st   ────────────┘└─
237    rw mem_image_eq,
id        └──────────┘
src    └─┘└──────────┘
typ    └─┘└──────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────────────┘└─
238    exact ⟨(y₁, z), ho (by simp [zs, yo₁]), rfl⟩
id             └┘     └┘           └┘  └─┘    └─┘
src    └────┘    └┘ └─┘     └────┘  └┘   └─┘└─┘└┘
typ    └────┘  └┘└┘└─┘└┘   └────┘└┘└┘└─┘└─┘└─┘└┘
doc    └────┘    └┘ └─┘     └────┘  └┘   └─┘   └┘
txt    └────┘    └┘ └─┘     └────┘  └┘   └─┘   └┘
par    └────┘    └┘ └─┘     └────┘  └┘   └─┘   └┘
pid             └┘ └─┘     └─────┘  └┘   └──┘   
st   ───────────────────────┘└─────────────┘└──────┘
239  end
st   └─┘
240  
241  /-- A product set is open in a product space if and only if each factor is open, or one of them is
242  empty -/
243  lemma is_open_prod_iff' {s : set α} {t : set β} :
id                                └─┘        └─┘ 
src                               └─┘         └─┘
typ                               └─┘        └─┘ 
244    is_open (set.prod s t) ↔ (is_open s ∧ is_open t) ∨ (s = ∅) ∨ (t = ∅) :=
id     └─────┘  └──────┘      └─────┘   └─────┘             
src    └─────┘  └──────┘        └─────┘    └─────┘                
typ    └─────┘  └──────┘      └─────┘   └─────┘             
doc    └─────┘  └──────┘         └─────┘     └─────┘
245  begin
st   └─────
246    cases (set.prod s t).eq_empty_or_nonempty with h h,
id            └──────┘  
src    └────┘ └──────┘  └─────────────────────────────┘
typ    └────┘ └──────┘└─────────────────────────────┘
doc    └────┘ └──────┘  └─────────────────────────────┘
txt    └────┘           └─────────────────────────────┘
par    └────┘           └─────────────────────────────┘
pid                    └───────────────────┘└────────┘
st   ───────────────────────────────────────────────────┘└─
247    { simp [h, prod_eq_empty_iff.1 h] },
id               └───────────────┘   
src      └────┘ └┘└───────────────┘└─┘ └┘
typ      └────┘└┘└───────────────┘└─┘└┘
doc      └────┘ └┘                 └─┘ └┘
txt      └────┘ └┘                 └─┘ └┘
par      └────┘ └┘                 └─┘ └┘
pid           └┘                 └─┘ 
st   ───┘└──────────────────────────────┘└┘
248    { have st : s.nonempty ∧ t.nonempty, from prod_nonempty_iff.1 h,
id                 └────────┘   └────────┘       └───────────────┘   
src      └────────┘└────────┘ └────────┘  └───┘└───────────────┘└─┘
typ      └────────┘└────────┘ └────────┘  └───┘└───────────────┘└─┘
doc      └────────┘└────────┘ └────────┘  └───┘                 └─┘
txt      └────────┘                       └───┘                 └─┘
par      └────────┘                       └───┘                 └─┘
pid      └─────┘└─┘                       └───┘                 └─┘
st   ────────────────────────────────────┘└──────────────────────────┘└─
249      split,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
250      { assume H : is_open (set.prod s t),
id                    └─────┘  └──────┘  
src        └─────────┘└─────┘ └──────┘  
typ        └─────────┘└─────┘ └──────┘
doc        └─────────┘└─────┘ └──────┘  
txt        └─────────┘                  
par        └─────────┘                  
pid        └─────────┘                  
st   ─────┘└───────────────────────────────┘└─
251        refine or.inl ⟨_, _⟩,
id                └────┘
src        └─────┘└────┘ └───┘
typ        └─────┘└────┘ └───┘
doc        └─────┘       └───┘
txt        └─────┘       └───┘
par        └─────┘       └───┘
pid                     └───┘
st   ─────────────────────────┘└─
252        show is_open s,
id              └─────┘ 
src        └───┘└─────┘
typ        └───┘└─────┘
doc        └───┘└─────┘
txt        └───┘       
par        └───┘       
pid        └───┘       
st   ──────────────────────
253        { rw ← fst_image_prod s st.2,
id                └────────────┘  └┘
src          └───┘└────────────┘   └┘
typ          └───┘└────────────┘└┘└┘
doc          └───┘                 └┘
txt          └───┘                 └┘
par          └───┘                 └┘
pid            └─┘                 └┘
st   ───────┘└────────────────────────┘└─
254          exact is_open_map_fst _ H },
id                 └─────────────┘   
src          └────┘└─────────────┘└─┘ 
typ          └────┘└─────────────┘└─┘
doc          └────┘└─────────────┘└─┘ 
txt          └────┘               └─┘ 
par          └────┘               └─┘ 
pid                              └─┘ 
st   ─────────────────────────────────┘└┘
255        show is_open t,
id              └─────┘ 
src        └───┘└─────┘
typ        └───┘└─────┘
doc        └───┘└─────┘
txt        └───┘       
par        └───┘       
pid        └───┘       
st   ──────────────────────
256        { rw ← snd_image_prod st.1 t,
id                └────────────┘ └┘   
src          └───┘└────────────┘  └─┘
typ          └───┘└────────────┘└┘└─┘
doc          └───┘                └─┘
txt          └───┘                └─┘
par          └───┘                └─┘
pid            └─┘                └─┘
st   ─────────────────────────────────┘└─
257          exact is_open_map_snd _ H } },
id                 └─────────────┘   
src          └────┘└─────────────┘└─┘ 
typ          └────┘└─────────────┘└─┘
doc          └────┘└─────────────┘└─┘ 
txt          └────┘               └─┘ 
par          └────┘               └─┘ 
pid                              └─┘ 
st   ─────────────────────────────────┘└──┘
258      { assume H,
src        └──────┘
typ        └──────┘
doc        └──────┘
txt        └──────┘
par        └──────┘
pid        └──────┘
st   ─────────────┘└─
259        simp [st.1.ne_empty, st.2.ne_empty] at H,
id               └┘             └┘
src        └────┘  └───────────┘  └───────────────┘
typ        └────┘└┘└───────────┘└┘└───────────────┘
doc        └────┘  └───────────┘  └───────────────┘
txt        └────┘  └───────────┘  └───────────────┘
par        └────┘  └───────────┘  └───────────────┘
pid              └───────────┘  └──────────┘└──┘
st   ─────────────────────────────────────────────┘└─
260        exact is_open_prod H.1 H.2 } }
id               └──────────┘     
src        └────┘└──────────┘ └─┘ └─┘
typ        └────┘└──────────┘ └─┘└─┘
doc        └────┘             └─┘ └─┘
txt        └────┘             └─┘ └─┘
par        └────┘             └─┘ └─┘
pid                          └─┘ └─┘
st   ────────────────────────────────┘└───
261  end
st   ──┘
262  
263  lemma closure_prod_eq {s : set α} {t : set β} :
id                              └─┘        └─┘ 
src                             └─┘         └─┘
typ                             └─┘        └─┘ 
264    closure (set.prod s t) = set.prod (closure s) (closure t) :=
id     └─────┘  └──────┘     └──────┘  └─────┘    └─────┘ 
src    └─────┘  └──────┘       └──────┘  └─────┘     └─────┘
typ    └─────┘  └──────┘     └──────┘  └─────┘    └─────┘ 
doc    └─────┘  └──────┘        └──────┘  └─────┘     └─────┘
265  set.ext $ assume ⟨a, b⟩,
id   └─────┘            
src  └─────┘
typ  └─────┘            
266  have filter.prod (𝓝 a) (𝓝 b) ⊓ principal (set.prod s t) =
id        └─────────┘            └───────┘  └──────┘    
src       └─────────┘            └───────┘  └──────┘      
typ       └─────────┘            └───────┘  └──────┘    
doc       └─────────┘             └───────┘  └──────┘
267    filter.prod (𝓝 a ⊓ principal s) (𝓝 b ⊓ principal t),
id     └─────────┘      └───────┘        └───────┘ 
src    └─────────┘      └───────┘         └───────┘
typ    └─────────┘      └───────┘        └───────┘ 
doc    └─────────┘       └───────┘          └───────┘
268    by rw [←prod_inf_prod, prod_principal_principal],
id             └───────────┘  └──────────────────────┘
src       └───┘└───────────┘└┘└──────────────────────┘
typ       └───┘└───────────┘└┘└──────────────────────┘
doc       └───┘             └┘                        
txt       └───┘             └┘                        
par       └───┘             └┘                        
pid         └─┘             └┘                        
st       └─────────────────┘└────────────────────────┘
269  by simp [closure_eq_nhds, nhds_prod_eq, this]; exact prod_ne_bot
id            └─────────────┘  └──────────┘  └──┘         └─────────┘
src     └────┘└─────────────┘└┘└──────────┘└┘      └────┘└─────────┘
typ     └────┘└─────────────┘└┘└──────────┘└┘└──┘  └────┘└─────────┘
doc     └────┘               └┘            └┘      └────┘           
txt     └────┘               └┘            └┘      └────┘           
par     └────┘               └┘            └┘      └────┘           
pid                        └┘            └┘                      
st     └──────────────────────────────────────────────────────────────
270  
src  
typ  
doc  
txt  
par  
pid  
st   
271  lemma mem_closure2 {s : set α} {t : set β} {u : set γ} {f : α → β → γ} {a : α} {b : β}
id                           └─┘        └─┘        └─┘                            
src                          └─┘         └─┘         └─┘
typ                          └─┘        └─┘        └─┘                            
272    (hf : continuous (λp:α×β, f p.1 p.2)) (ha : a ∈ closure s) (hb : b ∈ closure t)
id           └────────┘                      └─────┘           └─────┘ 
src          └────────┘                            └─────┘             └─────┘
typ          └────────┘                      └─────┘           └─────┘ 
doc          └────────┘                                └─────┘              └─────┘
273    (hu : ∀a b, a ∈ s → b ∈ t → f a b ∈ u) :
id                             
src                                    
typ                            
274    f a b ∈ closure u :=
id         └─────┘ 
src           └─────┘
typ        └─────┘ 
doc            └─────┘
275  have (a, b) ∈ closure (set.prod s t), by rw [closure_prod_eq]; from ⟨ha, hb⟩,
id             └─────┘  └──────┘            └─────────────┘         └┘  └┘
src              └─────┘  └──────┘          └──┘└─────────────┘  └───┘   └┘  
typ            └─────┘  └──────┘        └──┘└─────────────┘  └───┘ └┘└┘└┘
doc                └─────┘  └──────┘          └──┘                 └───┘   └┘  
txt                                           └──┘                 └───┘   └┘  
par                                           └──┘                 └───┘   └┘  
pid                                             └┘                 └───┘   └┘  
st                                           └──────────────────┘└─────────────┘
276  show (λp:α×β, f p.1 p.2) (a, b) ∈ closure u, from
id                         └─────┘ 
src                               └─────┘
typ                        └─────┘ 
doc                                    └─────┘
277    mem_closure hf this $ assume ⟨a, b⟩ ⟨ha, hb⟩, hu a b ha hb
id     └─────────┘ └┘ └──┘              └┘  └┘   └┘
src    └─────────┘
typ    └─────────┘ └┘ └──┘              └┘  └┘   └┘
278  
279  lemma is_closed_prod {s₁ : set α} {s₂ : set β} (h₁ : is_closed s₁) (h₂ : is_closed s₂) :
id                              └─┘         └─┘         └───────┘ └┘        └───────┘ └┘
src                             └─┘          └─┘          └───────┘           └───────┘
typ                             └─┘         └─┘         └───────┘ └┘        └───────┘ └┘
doc                                                       └───────┘           └───────┘
280    is_closed (set.prod s₁ s₂) :=
id     └───────┘  └──────┘ └┘ └┘
src    └───────┘  └──────┘
typ    └───────┘  └──────┘ └┘ └┘
doc    └───────┘  └──────┘
281  closure_eq_iff_is_closed.mp $ by simp [h₁, h₂, closure_prod_eq, closure_eq_of_is_closed]
id   └──────────────────────┘└─┘            └┘  └┘  └─────────────┘  └─────────────────────┘
src  └──────────────────────┘└─┘      └────┘  └┘  └┘└─────────────┘└┘└─────────────────────┘└─
typ  └──────────────────────┘└─┘      └────┘└┘└┘└┘└┘└─────────────┘└┘└─────────────────────┘└─
doc                                   └────┘  └┘  └┘               └┘                       └─
txt                                   └────┘  └┘  └┘               └┘                       └─
par                                   └────┘  └┘  └┘               └┘                       └─
pid                                         └┘  └┘               └┘                       
st                                   └────────────────────────────────────────────────────────
282  
src  
typ  
doc  
txt  
par  
pid  
st   
283  lemma inducing.prod_mk {f : α → β} {g : γ → δ} (hf : inducing f) (hg : inducing g) :
id                                                    └──────┘         └──────┘ 
src                                                       └──────┘          └──────┘
typ                                                   └──────┘         └──────┘ 
284    inducing (λx:α×γ, (f x.1, g x.2)) :=
id     └──────┘            
src    └──────┘                  
typ    └──────┘            
285  ⟨by rw [prod.topological_space, prod.topological_space, hf.induced, hg.induced,
id           └────────────────────┘  └────────────────────┘
src      └──┘└────────────────────┘└┘└────────────────────┘└┘          └┘          └─
typ      └──┘└────────────────────┘└┘└────────────────────┘└┘└────────┘└┘└────────┘└─
doc      └──┘                      └┘                      └┘          └┘          └─
txt      └──┘                      └┘                      └┘          └┘          └─
par      └──┘                      └┘                      └┘          └┘          └─
pid        └┘                      └┘                      └┘          └┘          └─
st      └─────────────────────────┘└──────────────────────┘└──────────┘└──────────┘└─
286           induced_compose, induced_compose, induced_inf, induced_compose, induced_compose]⟩
id            └─────────────┘  └─────────────┘  └─────────┘  └─────────────┘  └─────────────┘
src  ────────┘└─────────────┘└┘└─────────────┘└┘└─────────┘└┘└─────────────┘└┘└─────────────┘
typ  ────────┘└─────────────┘└┘└─────────────┘└┘└─────────┘└┘└─────────────┘└┘└─────────────┘
doc  ────────┘               └┘               └┘           └┘               └┘               
txt  ────────┘               └┘               └┘           └┘               └┘               
par  ────────┘               └┘               └┘           └┘               └┘               
pid  ────────┘               └┘               └┘           └┘               └┘               
st   ───────────────────────┘└───────────────┘└───────────┘└───────────────┘└───────────────┘
287  
288  lemma embedding.prod_mk {f : α → β} {g : γ → δ} (hf : embedding f) (hg : embedding g) :
id                                                     └───────┘         └───────┘ 
src                                                        └───────┘          └───────┘
typ                                                    └───────┘         └───────┘ 
doc                                                        └───────┘          └───────┘
289    embedding (λx:α×γ, (f x.1, g x.2)) :=
id     └───────┘            
src    └───────┘                  
typ    └───────┘            
doc    └───────┘
290  { inj := assume ⟨x₁, x₂⟩ ⟨y₁, y₂⟩, by simp; exact assume h₁ h₂, ⟨hf.inj h₁, hg.inj h₂⟩,
id                                                                  └────┘     └────┘
src                                        └──┘  └────┘      └──────┘ └────┘  └┘└────┘  
typ                                      └──┘  └────┘      └──────┘ └────┘  └┘└────┘  
doc                                        └──┘  └────┘      └──────┘         └┘        
txt                                        └──┘  └────┘      └──────┘         └┘        
par                                        └──┘  └────┘      └──────┘         └┘        
pid                                                         └──────┘         └┘        
st                                        └───────────────────────────────────────────────┘
291    ..hf.to_inducing.prod_mk hg.to_inducing }
id       └┘└──────────┘└──────┘ └┘└──────────┘
src        └──────────┘└──────┘   └──────────┘
typ      └┘└──────────┘└──────┘ └┘└──────────┘
292  
293  protected lemma is_open_map.prod {f : α → β} {g : γ → δ} (hf : is_open_map f) (hg : is_open_map g) :
id                                                              └─────────┘         └─────────┘ 
src                                                                 └─────────┘          └─────────┘
typ                                                             └─────────┘         └─────────┘ 
doc                                                                 └─────────┘          └─────────┘
294    is_open_map (λ p : α × γ, (f p.1, g p.2)) :=
id     └─────────┘                 
src    └─────────┘                       
typ    └─────────┘                 
doc    └─────────┘
295  begin
st   └─────
296    rw [is_open_map_iff_nhds_le],
id         └─────────────────────┘
src    └──┘└─────────────────────┘
typ    └──┘└─────────────────────┘
doc    └──┘                       
txt    └──┘                       
par    └──┘                       
pid      └┘                       
st   ────────────────────────────┘└──
297    rintros ⟨a, b⟩,
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid           └─────┘
st   ───────────────┘└─
298    rw [nhds_prod_eq, nhds_prod_eq, ← filter.prod_map_map_eq],
id         └──────────┘  └──────────┘    └────────────────────┘
src    └──┘└──────────┘└┘└──────────┘└──┘└────────────────────┘
typ    └──┘└──────────┘└┘└──────────┘└──┘└────────────────────┘
doc    └──┘            └┘            └──┘                      
txt    └──┘            └┘            └──┘                      
par    └──┘            └┘            └──┘                      
pid      └┘            └┘            └──┘                      
st   ─────────────────┘└────────────┘└────────────────────────┘└──
299    exact filter.prod_mono (is_open_map_iff_nhds_le.1 hf a) (is_open_map_iff_nhds_le.1 hg b)
id           └──────────────┘                            └┘    └─────────────────────┘   └┘ 
src    └────┘└──────────────┘                        └─┘   └┘ └─────────────────────┘└─┘   └┘
typ    └────┘└──────────────┘                        └─┘└┘└┘ └─────────────────────┘└─┘└┘└┘
doc    └────┘                                        └─┘   └┘                        └─┘   └┘
txt    └────┘                                        └─┘   └┘                        └─┘   └┘
par    └────┘                                        └─┘   └┘                        └─┘   └┘
pid                                                 └─┘   └┘                        └─┘   
st   ──────────────────────────────────────────────────────────────────────────────────────────┘
300  end
st   └─┘
301  
302  protected lemma open_embedding.prod {f : α → β} {g : γ → δ}
id                                                         
typ                                                        
303    (hf : open_embedding f) (hg : open_embedding g) : open_embedding (λx:α×γ, (f x.1, g x.2)) :=
id           └────────────┘         └────────────┘     └────────────┘            
src          └────────────┘          └────────────┘      └────────────┘                  
typ          └────────────┘         └────────────┘     └────────────┘            
doc          └────────────┘          └────────────┘      └────────────┘
304  open_embedding_of_embedding_open (hf.1.prod_mk hg.1)
id   └──────────────────────────────┘  └┘ └─────┘  └┘
src  └──────────────────────────────┘     └─────┘    
typ  └──────────────────────────────┘  └┘ └─────┘  └┘
305    (hf.is_open_map.prod hg.is_open_map)
id      └┘└──────────┘└───┘ └┘└──────────┘
src       └──────────┘└───┘   └──────────┘
typ     └┘└──────────┘└───┘ └┘└──────────┘
306  
307  lemma embedding_graph {f : α → β} (hf : continuous f) : embedding (λx, (x, f x)) :=
id                                         └────────┘     └───────┘        
src                                          └────────┘      └───────┘      
typ                                        └────────┘     └───────┘        
doc                                          └────────┘      └───────┘
308  embedding_of_embedding_compose (continuous_id.prod_mk hf) continuous_fst embedding_id
id   └────────────────────────────┘  └───────────┘└──────┘ └┘  └────────────┘ └──────────┘
src  └────────────────────────────┘  └───────────┘└──────┘     └────────────┘ └──────────┘
typ  └────────────────────────────┘  └───────────┘└──────┘ └┘  └────────────┘ └──────────┘
309  
310  end prod
311  
312  section sum
313  variables [topological_space α] [topological_space β] [topological_space γ]
id              └───────────────┘     └───────────────┘     └───────────────┘
src             └───────────────┘     └───────────────┘     └───────────────┘
typ             └───────────────┘     └───────────────┘     └───────────────┘
doc             └───────────────┘     └───────────────┘     └───────────────┘
314  
315  lemma continuous_inl : continuous (@sum.inl α β) :=
id                          └────────┘   └─────┘  
src                         └────────┘   └─────┘
typ                         └────────┘   └─────┘  
doc                         └────────┘
316  continuous_sup_rng_left continuous_coinduced_rng
id   └─────────────────────┘ └──────────────────────┘
src  └─────────────────────┘ └──────────────────────┘
typ  └─────────────────────┘ └──────────────────────┘
317  
318  lemma continuous_inr : continuous (@sum.inr α β) :=
id                          └────────┘   └─────┘  
src                         └────────┘   └─────┘
typ                         └────────┘   └─────┘  
doc                         └────────┘
319  continuous_sup_rng_right continuous_coinduced_rng
id   └──────────────────────┘ └──────────────────────┘
src  └──────────────────────┘ └──────────────────────┘
typ  └──────────────────────┘ └──────────────────────┘
320  
321  lemma continuous_sum_rec {f : α → γ} {g : β → γ}
id                                              
typ                                             
322    (hf : continuous f) (hg : continuous g) : @continuous (α ⊕ β) γ _ _ (@sum.rec α β (λ_, γ) f g) :=
id           └────────┘         └────────┘      └────────┘             └─────┘          
src          └────────┘          └────────┘       └────────┘                └─────┘
typ          └────────┘         └────────┘      └────────┘             └─────┘          
doc          └────────┘          └────────┘       └────────┘
323  continuous_sup_dom hf hg
id   └────────────────┘ └┘ └┘
src  └────────────────┘
typ  └────────────────┘ └┘ └┘
324  
325  lemma embedding_inl : embedding (@sum.inl α β) :=
id                         └───────┘   └─────┘  
src                        └───────┘   └─────┘
typ                        └───────┘   └─────┘  
doc                        └───────┘
326  { induced := begin
st                └─────
327      unfold sum.topological_space,
src      └──────────────────────────┘
typ      └──────────────────────────┘
doc      └──────────────────────────┘
txt      └──────────────────────────┘
par      └──────────────────────────┘
pid            └────────────────────┘
st   ───────────────────────────────┘└─
328      apply le_antisymm,
id             └─────────┘
src      └────┘└─────────┘
typ      └────┘└─────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ────────────────────┘└─
329      { rw ← coinduced_le_iff_le_induced, exact lattice.le_sup_left },
id              └─────────────────────────┘        └─────────────────┘
src        └───┘└─────────────────────────┘  └────┘└─────────────────┘
typ        └───┘└─────────────────────────┘  └────┘└─────────────────┘
doc        └───┘                             └────┘                   
txt        └───┘                             └────┘                   
par        └───┘                             └────┘                   
pid          └─┘                                                     
st   ─────┘└──────────────────────────────┘└──────────────────────────┘└┘
330      { intros u hu, existsi (sum.inl '' u),
id                               └─────┘ └┘ 
src        └─────────┘  └──────┘ └─────┘└┘ 
typ        └─────────┘  └──────┘ └─────┘└┘
doc        └─────────┘  └──────┘           
txt        └─────────┘  └──────┘           
par        └─────────┘  └──────┘           
pid              └───┘                    
st   ────────────────┘└──────────────────────┘└─
331        change
src        └──────
typ        └──────
doc        └──────
txt        └──────
par        └──────
pid              
st   ─────────────
332          (is_open (sum.inl ⁻¹' (@sum.inl α β '' u)) ∧
id                             └─┘
src  ───────┘                └─┘              └─┘ 
typ  ───────┘                └─┘              └─┘ 
doc  ───────┘                └─┘              └─┘ 
txt  ───────┘                                 └─┘ 
par  ───────┘                                 └─┘ 
pid  ───────┘                                 └─┘ 
st   ─────────────────────────────────────────────────────
333           is_open (sum.inr ⁻¹' (@sum.inl α β '' u))) ∧
id            └─────┘  └─────┘                
src  ────────┘└─────┘ └─────┘                 └──┘ 
typ  ────────┘└─────┘ └─────┘               └──┘ 
doc  ────────┘└─────┘                         └──┘ 
txt  ────────┘                                └──┘ 
par  ────────┘                                └──┘ 
pid  ────────┘                                └──┘ 
st   ──────────────────────────────────────────────────────
334          sum.inl ⁻¹' (sum.inl '' u) = u,
id                        └─────┘        
src  ───────┘           └─────┘   └┘
typ  ───────┘           └─────┘   └┘
doc  ───────┘                     └┘ 
txt  ───────┘                     └┘ 
par  ───────┘                     └┘ 
pid  ───────┘                     └┘ 
st   ─────────────────────────────────────┘└─
335        have : sum.inl ⁻¹' (@sum.inl α β '' u) = u :=
id                              └─────┘           
src        └─────┘            └─────┘     └┘  └───
typ        └─────┘            └─────┘   └┘ └───
doc        └─────┘                        └┘  └───
txt        └─────┘                        └┘  └───
par        └─────┘                        └┘  └───
pid        └───┘└┘                        └┘  └───
st   ────────────────────────────────────────────────────
336          preimage_image_eq u (λ _ _, sum.inl.inj_iff.mp), rw this,
id           └───────────────┘          └────────────────┘      └──┘
src  ───────┘└───────────────┘   └────┘└────────────────┘  └─┘
typ  ───────┘└───────────────┘  └────┘└────────────────┘  └─┘└──┘
doc  ───────┘                    └────┘                    └─┘
txt  ───────┘                    └────┘                    └─┘
par  ───────┘                    └────┘                    └─┘
pid  ───────┘                    └────┘                      
st   ──────────────────────────────────────────────────────┘└───────┘└─
337        have : sum.inr ⁻¹' (@sum.inl α β '' u) = ∅ :=
id                └─────┘       └─────┘          
src        └─────┘└─────┘     └─────┘     └┘ └───
typ        └─────┘└─────┘     └─────┘  └┘ └───
doc        └─────┘                        └┘  └───
txt        └─────┘                        └┘  └───
par        └─────┘                        └┘  └───
pid        └───┘└┘                        └┘  └───
st   ────────────────────────────────────────────────────
338          eq_empty_iff_forall_not_mem.mpr (assume a ⟨b, _, h⟩, sum.inl_ne_inr h), rw this,
id           └─────────────────────────────┘                     └────────────┘        └──┘
src  ───────┘└─────────────────────────────┘       └──┘ └───┘ └─┘└────────────┘   └─┘
typ  ───────┘└─────────────────────────────┘       └──┘ └───┘└─┘└────────────┘   └─┘└──┘
doc  ───────┘                                      └──┘ └───┘ └─┘                 └─┘
txt  ───────┘                                      └──┘ └───┘ └─┘                 └─┘
par  ───────┘                                      └──┘ └───┘ └─┘                 └─┘
pid  ───────┘                                      └──┘ └───┘ └─┘                   
st   ─────────────────────────────────────────────────────────────────────────────┘└───────┘└─
339        exact ⟨⟨hu, is_open_empty⟩, rfl⟩ }
id                 └┘  └───────────┘   └─┘
src        └────┘    └┘└───────────┘└─┘└─┘└┘
typ        └────┘  └┘└┘└───────────┘└─┘└─┘└┘
doc        └────┘    └┘             └─┘   └┘
txt        └────┘    └┘             └─┘   └┘
par        └────┘    └┘             └─┘   └┘
pid                 └┘             └─┘   
st   ──────────────────────────────────────┘└─
340    end,
st   ────┘
341    inj := λ _ _, sum.inl.inj_iff.mp }
id                 └─────────────┘└─┘
src                  └─────────────┘└─┘
typ                └─────────────┘└─┘
342  
343  lemma embedding_inr : embedding (@sum.inr α β) :=
id                         └───────┘   └─────┘  
src                        └───────┘   └─────┘
typ                        └───────┘   └─────┘  
doc                        └───────┘
344  { induced := begin
st                └─────
345      unfold sum.topological_space,
src      └──────────────────────────┘
typ      └──────────────────────────┘
doc      └──────────────────────────┘
txt      └──────────────────────────┘
par      └──────────────────────────┘
pid            └────────────────────┘
st   ───────────────────────────────┘└─
346      apply le_antisymm,
id             └─────────┘
src      └────┘└─────────┘
typ      └────┘└─────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ────────────────────┘└─
347      { rw ← coinduced_le_iff_le_induced, exact lattice.le_sup_right },
id              └─────────────────────────┘        └──────────────────┘
src        └───┘└─────────────────────────┘  └────┘└──────────────────┘
typ        └───┘└─────────────────────────┘  └────┘└──────────────────┘
doc        └───┘                             └────┘                    
txt        └───┘                             └────┘                    
par        └───┘                             └────┘                    
pid          └─┘                                                      
st   ─────┘└──────────────────────────────┘└───────────────────────────┘└┘
348      { intros u hu, existsi (sum.inr '' u),
id                               └─────┘ └┘ 
src        └─────────┘  └──────┘ └─────┘└┘ 
typ        └─────────┘  └──────┘ └─────┘└┘
doc        └─────────┘  └──────┘           
txt        └─────────┘  └──────┘           
par        └─────────┘  └──────┘           
pid              └───┘                    
st   ────────────────┘└──────────────────────┘└─
349        change
src        └──────
typ        └──────
doc        └──────
txt        └──────
par        └──────
pid              
st   ─────────────
350          (is_open (sum.inl ⁻¹' (@sum.inr α β '' u)) ∧
id                     └─────┘ └─┘
src  ───────┘         └─────┘└─┘              └─┘ 
typ  ───────┘         └─────┘└─┘              └─┘ 
doc  ───────┘                └─┘              └─┘ 
txt  ───────┘                                 └─┘ 
par  ───────┘                                 └─┘ 
pid  ───────┘                                 └─┘ 
st   ─────────────────────────────────────────────────────
351           is_open (sum.inr ⁻¹' (@sum.inr α β '' u))) ∧
id            └─────┘                         
src  ────────┘└─────┘                         └──┘ 
typ  ────────┘└─────┘                       └──┘ 
doc  ────────┘└─────┘                         └──┘ 
txt  ────────┘                                └──┘ 
par  ────────┘                                └──┘ 
pid  ────────┘                                └──┘ 
st   ──────────────────────────────────────────────────────
352          sum.inr ⁻¹' (sum.inr '' u) = u,
id                        └─────┘        
src  ───────┘           └─────┘   └┘
typ  ───────┘           └─────┘   └┘
doc  ───────┘                     └┘ 
txt  ───────┘                     └┘ 
par  ───────┘                     └┘ 
pid  ───────┘                     └┘ 
st   ─────────────────────────────────────┘└─
353        have : sum.inl ⁻¹' (@sum.inr α β '' u) = ∅ :=
id                └─────┘       └─────┘          
src        └─────┘└─────┘     └─────┘     └┘ └───
typ        └─────┘└─────┘     └─────┘  └┘ └───
doc        └─────┘                        └┘  └───
txt        └─────┘                        └┘  └───
par        └─────┘                        └┘  └───
pid        └───┘└┘                        └┘  └───
st   ────────────────────────────────────────────────────
354          eq_empty_iff_forall_not_mem.mpr (assume b ⟨a, _, h⟩, sum.inr_ne_inl h), rw this,
id           └─────────────────────────────┘                     └────────────┘        └──┘
src  ───────┘└─────────────────────────────┘       └──┘ └───┘ └─┘└────────────┘   └─┘
typ  ───────┘└─────────────────────────────┘       └──┘ └───┘└─┘└────────────┘   └─┘└──┘
doc  ───────┘                                      └──┘ └───┘ └─┘                 └─┘
txt  ───────┘                                      └──┘ └───┘ └─┘                 └─┘
par  ───────┘                                      └──┘ └───┘ └─┘                 └─┘
pid  ───────┘                                      └──┘ └───┘ └─┘                   
st   ─────────────────────────────────────────────────────────────────────────────┘└───────┘└─
355        have : sum.inr ⁻¹' (@sum.inr α β '' u) = u :=
id                              └─────┘           
src        └─────┘            └─────┘     └┘  └───
typ        └─────┘            └─────┘   └┘ └───
doc        └─────┘                        └┘  └───
txt        └─────┘                        └┘  └───
par        └─────┘                        └┘  └───
pid        └───┘└┘                        └┘  └───
st   ────────────────────────────────────────────────────
356          preimage_image_eq u (λ _ _, sum.inr.inj_iff.mp), rw this,
id           └───────────────┘          └────────────────┘      └──┘
src  ───────┘└───────────────┘   └────┘└────────────────┘  └─┘
typ  ───────┘└───────────────┘  └────┘└────────────────┘  └─┘└──┘
doc  ───────┘                    └────┘                    └─┘
txt  ───────┘                    └────┘                    └─┘
par  ───────┘                    └────┘                    └─┘
pid  ───────┘                    └────┘                      
st   ──────────────────────────────────────────────────────┘└───────┘└─
357        exact ⟨⟨is_open_empty, hu⟩, rfl⟩ }
id                 └───────────┘  └┘   └─┘
src        └────┘  └───────────┘└┘  └─┘└─┘└┘
typ        └────┘  └───────────┘└┘└┘└─┘└─┘└┘
doc        └────┘               └┘  └─┘   └┘
txt        └────┘               └┘  └─┘   └┘
par        └────┘               └┘  └─┘   └┘
pid                            └┘  └─┘   
st   ──────────────────────────────────────┘└─
358    end,
st   ────┘
359    inj := λ _ _, sum.inr.inj_iff.mp }
id                 └─────────────┘└─┘
src                  └─────────────┘└─┘
typ                └─────────────┘└─┘
360  
361  end sum
362  
363  section subtype
364  variables [topological_space α] [topological_space β] [topological_space γ] {p : α → Prop}
id              └───────────────┘     └───────────────┘     └───────────────┘
src             └───────────────┘     └───────────────┘     └───────────────┘
typ             └───────────────┘     └───────────────┘     └───────────────┘
doc             └───────────────┘     └───────────────┘     └───────────────┘
365  
366  lemma embedding_subtype_val : embedding (@subtype.val α p) :=
id                                 └───────┘   └─────────┘  
src                                └───────┘   └─────────┘
typ                                └───────┘   └─────────┘  
doc                                └───────┘
367  ⟨⟨rfl⟩, subtype.val_injective⟩
id     └─┘   └───────────────────┘
src    └─┘   └───────────────────┘
typ    └─┘   └───────────────────┘
368  
369  lemma continuous_subtype_val : continuous (@subtype.val α p) :=
id                                  └────────┘   └─────────┘  
src                                 └────────┘   └─────────┘
typ                                 └────────┘   └─────────┘  
doc                                 └────────┘
370  continuous_induced_dom
id   └────────────────────┘
src  └────────────────────┘
typ  └────────────────────┘
371  
372  lemma is_open.open_embedding_subtype_val {s : set α} (hs : is_open s) :
id                                                 └─┘         └─────┘ 
src                                                └─┘          └─────┘
typ                                                └─┘         └─────┘ 
doc                                                             └─────┘
373    open_embedding (subtype.val : s → α) :=
id     └────────────┘  └─────────┘      
src    └────────────┘  └─────────┘
typ    └────────────┘  └─────────┘      
doc    └────────────┘
374  { induced := rfl,
id                └─┘
src               └─┘
typ               └─┘
375    inj := subtype.val_injective,
id            └───────────────────┘
src           └───────────────────┘
typ           └───────────────────┘
376    open_range := (subtype.val_range : range subtype.val = s).symm ▸  hs }
id                    └───────────────┘   └───┘ └─────────┘   └──┘    └┘
src                   └───────────────┘   └───┘ └─────────┘    └──┘  
typ                   └───────────────┘   └───┘ └─────────┘   └──┘    └┘
doc                                       └───┘
377  
378  lemma is_open.is_open_map_subtype_val {s : set α} (hs : is_open s) :
id                                              └─┘         └─────┘ 
src                                             └─┘          └─────┘
typ                                             └─┘         └─────┘ 
doc                                                          └─────┘
379    is_open_map (subtype.val : s → α) :=
id     └─────────┘  └─────────┘      
src    └─────────┘  └─────────┘
typ    └─────────┘  └─────────┘      
doc    └─────────┘
380  hs.open_embedding_subtype_val.is_open_map
id   └┘└─────────────────────────┘└──────────┘
src    └─────────────────────────┘└──────────┘
typ  └┘└─────────────────────────┘└──────────┘
381  
382  lemma is_open_map.restrict {f : α → β} (hf : is_open_map f) {s : set α} (hs : is_open s) :
id                                              └─────────┘        └─┘         └─────┘ 
src                                               └─────────┘         └─┘          └─────┘
typ                                             └─────────┘        └─┘         └─────┘ 
doc                                               └─────────┘                      └─────┘
383    is_open_map (function.restrict f s) :=
id     └─────────┘  └───────────────┘  
src    └─────────┘  └───────────────┘
typ    └─────────┘  └───────────────┘  
doc    └─────────┘
384  hf.comp hs.is_open_map_subtype_val
id   └┘└───┘ └┘└──────────────────────┘
src    └───┘   └──────────────────────┘
typ  └┘└───┘ └┘└──────────────────────┘
385  
386  lemma is_closed.closed_embedding_subtype_val {s : set α} (hs : is_closed s) :
id                                                     └─┘         └───────┘ 
src                                                    └─┘          └───────┘
typ                                                    └─┘         └───────┘ 
doc                                                                 └───────┘
387    closed_embedding (subtype.val : {x // x ∈ s} → α) :=
id     └──────────────┘  └─────────┘             
src    └──────────────┘  └─────────┘          
typ    └──────────────┘  └─────────┘             
doc    └──────────────┘
388  { induced := rfl,
id                └─┘
src               └─┘
typ               └─┘
389    inj := subtype.val_injective,
id            └───────────────────┘
src           └───────────────────┘
typ           └───────────────────┘
390    closed_range := (subtype.val_range : range subtype.val = s).symm ▸ hs }
id                      └───────────────┘   └───┘ └─────────┘   └──┘   └┘
src                     └───────────────┘   └───┘ └─────────┘    └──┘  
typ                     └───────────────┘   └───┘ └─────────┘   └──┘   └┘
doc                                         └───┘
391  
392  lemma continuous_subtype_mk {f : β → α}
id                                       
typ                                      
393    (hp : ∀x, p (f x)) (h : continuous f) : continuous (λx, (⟨f x, hp x⟩ : subtype p)) :=
id                         └────────┘     └────────┘          └┘     └─────┘ 
src                            └────────┘      └────────┘                     └─────┘
typ                        └────────┘     └────────┘          └┘     └─────┘ 
doc                            └────────┘      └────────┘
394  continuous_induced_rng h
id   └────────────────────┘ 
src  └────────────────────┘
typ  └────────────────────┘ 
395  
396  lemma continuous_inclusion {s t : set α} (h : s ⊆ t) : continuous (inclusion h) :=
id                                     └─┘              └────────┘  └───────┘ 
src                                    └─┘                 └────────┘  └───────┘
typ                                    └─┘              └────────┘  └───────┘ 
doc                                                         └────────┘  └───────┘
397  continuous_subtype_mk _ continuous_subtype_val
id   └───────────────────┘   └────────────────────┘
src  └───────────────────┘   └────────────────────┘
typ  └───────────────────┘   └────────────────────┘
398  
399  lemma continuous_at_subtype_val {p : α → Prop} {a : subtype p} :
id                                                      └─────┘ 
src                                                      └─────┘
typ                                                     └─────┘ 
400    continuous_at subtype.val a :=
id     └───────────┘ └─────────┘ 
src    └───────────┘ └─────────┘
typ    └───────────┘ └─────────┘ 
doc    └───────────┘
401  continuous_iff_continuous_at.mp continuous_subtype_val _
id   └──────────────────────────┘└─┘ └────────────────────┘
src  └──────────────────────────┘└─┘ └────────────────────┘
typ  └──────────────────────────┘└─┘ └────────────────────┘
402  
403  lemma map_nhds_subtype_val_eq {a : α} (ha : p a) (h : {a | p a} ∈ 𝓝 a) :
id                                                              
src                                                                  
typ                                                             
doc                                                                    
404    map (@subtype.val α p) (𝓝 ⟨a, ha⟩) = 𝓝 a :=
id     └─┘   └─────────┘         └┘     
src    └─┘   └─────────┘                  
typ    └─┘   └─────────┘         └┘     
doc    └─┘                                 
405  map_nhds_induced_eq (by simp [subtype.val_image, h])
id   └─────────────────┘           └───────────────┘  
src  └─────────────────┘     └────┘└───────────────┘└┘ 
typ  └─────────────────┘     └────┘└───────────────┘└┘
doc                          └────┘                 └┘ 
txt                          └────┘                 └┘ 
par                          └────┘                 └┘ 
pid                                               └┘ 
st                          └──────────────────────────┘
406  
407  lemma nhds_subtype_eq_comap {a : α} {h : p a} :
id                                            
typ                                           
408    𝓝 (⟨a, h⟩ : subtype p) = comap subtype.val (𝓝 a) :=
id              └─────┘    └───┘ └─────────┘   
src               └─────┘     └───┘ └─────────┘  
typ             └─────┘    └───┘ └─────────┘   
doc                            └───┘              
409  nhds_induced _ _
id   └──────────┘
src  └──────────┘
typ  └──────────┘
410  
411  lemma tendsto_subtype_rng {β : Type*} {p : α → Prop} {b : filter β} {f : β → subtype p} :
id                                                            └────┘           └─────┘ 
src                                                            └────┘             └─────┘
typ                                                           └────┘           └─────┘ 
412    ∀{a:subtype p}, tendsto f b (𝓝 a) ↔ tendsto (λx, subtype.val (f x)) b (𝓝 a.val)
id        └─────┘    └─────┘        └─────┘     └─────────┘         └──┘
src        └─────┘     └─────┘           └─────┘      └─────────┘             └──┘
typ       └─────┘    └─────┘        └─────┘     └─────────┘         └──┘
doc                    └─────┘            └─────┘                            
413  | ⟨a, ha⟩ := by rw [nhds_subtype_eq_comap, tendsto_comap_iff]
id                       └───────────────────┘  └───────────────┘
src                  └──┘└───────────────────┘└┘└───────────────┘└─
typ                  └──┘└───────────────────┘└┘└───────────────┘└─
doc                  └──┘                     └┘                 └─
txt                  └──┘                     └┘                 └─
par                  └──┘                     └┘                 └─
pid                    └┘                     └┘                 
st                  └────────────────────────┘└─────────────────┘
414  
src  
typ  
doc  
txt  
par  
pid  
st   
415  lemma continuous_subtype_nhds_cover {ι : Sort*} {f : α → β} {c : ι → α → Prop}
id                                                                     
typ                                                                    
416    (c_cover : ∀x:α, ∃i, {x | c i x} ∈ 𝓝 x)
id                               
src                                   
typ                              
doc                                       
417    (f_cont  : ∀i, continuous (λ(x : subtype (c i)), f x.val)) :
id                   └────────┘        └─────┘        └──┘
src                   └────────┘        └─────┘            └──┘
typ                  └────────┘        └─────┘        └──┘
doc                   └────────┘
418    continuous f :=
id     └────────┘ 
src    └────────┘
typ    └────────┘ 
doc    └────────┘
419  continuous_iff_continuous_at.mpr $ assume x,
id   └──────────────────────────┘└──┘          
src  └──────────────────────────┘└──┘
typ  └──────────────────────────┘└──┘          
420    let ⟨i, (c_sets : {x | c i x} ∈ 𝓝 x)⟩ := c_cover x in
id     └─┘                             └─────┘ 
src                                  
typ    └─┘                             └─────┘ 
doc                                    
421    let x' : subtype (c i) := ⟨x, mem_of_nhds c_sets⟩ in
id              └─────┘            └─────────┘
src             └─────┘              └─────────┘
typ             └─────┘            └─────────┘
422    calc map f (𝓝 x) = map f (map subtype.val (𝓝 x')) :
id          └─┘        └─┘   └─┘ └─────────┘   └┘
src         └─┘          └─┘    └─┘ └─────────┘  
typ         └─┘        └─┘   └─┘ └─────────┘   └┘
doc         └─┘          └─┘    └─┘              
423        congr_arg (map f) (map_nhds_subtype_val_eq _ $ c_sets).symm
id         └───────┘  └─┘    └─────────────────────┘            └──┘
src        └───────┘  └─┘     └─────────────────────┘            └──┘
typ        └───────┘  └─┘    └─────────────────────┘            └──┘
doc                   └─┘
424      ... = map (λx:subtype (c i), f x.val) (𝓝 x') : rfl
id             └─┘     └─────┘        └──┘    └┘    └─┘
src            └─┘     └─────┘           └──┘          └─┘
typ            └─┘     └─────┘        └──┘    └┘    └─┘
doc            └─┘                              
425      ... ≤ 𝓝 (f x) : continuous_iff_continuous_at.mp (f_cont i) x'
id                    └──────────────────────────┘└─┘  └────┘    └┘
src                     └──────────────────────────┘└─┘
typ                   └──────────────────────────┘└─┘  └────┘    └┘
doc            
426  
427  lemma continuous_subtype_is_closed_cover {ι : Sort*} {f : α → β} (c : ι → α → Prop)
id                                                                          
typ                                                                         
428    (h_lf : locally_finite (λi, {x | c i x}))
id             └────────────┘          
src            └────────────┘      
typ            └────────────┘          
doc            └────────────┘
429    (h_is_closed : ∀i, is_closed {x | c i x})
id                       └───────┘      
src                       └───────┘ 
typ                      └───────┘      
doc                       └───────┘
430    (h_cover : ∀x, ∃i, c i x)
id                      
src                    
typ                     
431    (f_cont  : ∀i, continuous (λ(x : subtype (c i)), f x.val)) :
id                   └────────┘        └─────┘        └──┘
src                   └────────┘        └─────┘            └──┘
typ                  └────────┘        └─────┘        └──┘
doc                   └────────┘
432    continuous f :=
id     └────────┘ 
src    └────────┘
typ    └────────┘ 
doc    └────────┘
433  continuous_iff_is_closed.mpr $
id   └──────────────────────┘└──┘
src  └──────────────────────┘└──┘
typ  └──────────────────────┘└──┘
434    assume s hs,
id             └┘
typ            └┘
435    have ∀i, is_closed (@subtype.val α {x | c i x} '' (f ∘ subtype.val ⁻¹' s)),
id             └───────┘   └─────────┘         └┘    └─────────┘ └─┘ 
src             └───────┘   └─────────┘              └┘     └─────────┘ └─┘
typ            └───────┘   └─────────┘         └┘    └─────────┘ └─┘ 
doc             └───────┘                                                 └─┘
436      from assume i,
id                   
typ                  
437      embedding_is_closed embedding_subtype_val
id       └─────────────────┘ └───────────────────┘
src      └─────────────────┘ └───────────────────┘
typ      └─────────────────┘ └───────────────────┘
438        (by simp [subtype.val_range]; exact h_is_closed i)
id                   └───────────────┘         └─────────┘ 
src            └────┘└───────────────┘  └────┘           
typ            └────┘└───────────────┘  └────┘└─────────┘
doc            └────┘                   └────┘           
txt            └────┘                   └────┘           
par            └────┘                   └────┘           
pid                                                   
st            └────────────────────────────────────────────┘
439        (continuous_iff_is_closed.mp (f_cont i) _ hs),
id          └──────────────────────┘└─┘  └────┘     └┘
src         └──────────────────────┘└─┘
typ         └──────────────────────┘└─┘  └────┘     └┘
440    have is_closed (⋃i, @subtype.val α {x | c i x} '' (f ∘ subtype.val ⁻¹' s)),
id          └───────┘    └─────────┘         └┘    └─────────┘ └─┘ 
src         └───────┘     └─────────┘              └┘     └─────────┘ └─┘
typ         └───────┘    └─────────┘         └┘    └─────────┘ └─┘ 
doc         └───────┘                                                   └─┘
441      from is_closed_Union_of_locally_finite
id            └───────────────────────────────┘
src           └───────────────────────────────┘
typ           └───────────────────────────────┘
442        (locally_finite_subset h_lf $ assume i x ⟨⟨x', hx'⟩, _, heq⟩, heq ▸ hx')
id          └───────────────────┘ └──┘                 └─┘      └─┘       
src         └───────────────────┘                                  └─┘       
typ         └───────────────────┘ └──┘                 └─┘      └─┘       
443        this,
id         └──┘
typ        └──┘
444    have f ⁻¹' s = (⋃i, @subtype.val α {x | c i x} '' (f ∘ subtype.val ⁻¹' s)),
id           └─┘      └─────────┘         └┘    └─────────┘ └─┘ 
src           └─┘        └─────────┘              └┘     └─────────┘ └─┘
typ          └─┘      └─────────┘         └┘    └─────────┘ └─┘ 
doc           └─┘                                                       └─┘
445    begin
st     └─────
446      apply set.ext,
id             └─────┘
src      └────┘└─────┘
typ      └────┘└─────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ────────────────┘└─
447      have : ∀ (x : α), f x ∈ s ↔ ∃ (i : ι), c i x ∧ f x ∈ s :=
id                                                    
src      └─────┘ └────┘      └────┘        └───
typ      └─────┘ └────┘     └────┘    └───
doc      └─────┘ └────┘        └────┘          └───
txt      └─────┘ └────┘        └────┘          └───
par      └─────┘ └────┘        └────┘          └───
pid      └───┘└┘ └────┘        └────┘          └───
st   ──────────────────────────────────────────────────────────────
448        λ x, ⟨λ hx, let ⟨i, hi⟩ := h_cover x in ⟨i, hi, hx⟩,
id                            └┘     └─────┘
src  ─────┘ └──┘  └───┘     └┘  └───┘        └──┘  └┘  └┘  └──
typ  ─────┘ └──┘  └───┘    └┘└┘└───┘└─────┘ └──┘  └┘  └┘  └──
doc  ─────┘ └──┘  └───┘     └┘  └───┘        └──┘  └┘  └┘  └──
txt  ─────┘ └──┘  └───┘     └┘  └───┘        └──┘  └┘  └┘  └──
par  ─────┘ └──┘  └───┘     └┘  └───┘        └──┘  └┘  └┘  └──
pid  ─────┘ └──┘  └───┘     └┘  └───┘        └──┘  └┘  └┘  └──
st   ───────────────────────────────────────────────────────────
449              λ ⟨i, hi, hx⟩, hx⟩,
id                         └┘
src  ───────────┘ └┘ └┘  └┘  └─┘  
typ  ───────────┘ └┘ └┘  └┘└┘└─┘  
doc  ───────────┘ └┘ └┘  └┘  └─┘  
txt  ───────────┘ └┘ └┘  └┘  └─┘  
par  ───────────┘ └┘ └┘  └┘  └─┘  
pid  ───────────┘ └┘ └┘  └┘  └─┘  
st   ─────────────────────────────┘└─
450      simp [and.comm, and.left_comm], simpa [(∘)],
id             └──────┘  └───────────┘          
src      └────┘└──────┘└┘└───────────┘  └─────┘└─┘
typ      └────┘└──────┘└┘└───────────┘  └─────┘└─┘
doc      └────┘        └┘               └─────┘ └─┘
txt      └────┘        └┘               └─────┘ └─┘
par      └────┘        └┘               └─────┘ └─┘
pid                  └┘                     └─┘
st   ─────────────────────────────────┘└───────────┘└─
451    end,
st   ────┘
452    by rwa [this]
id             └──┘
src       └───┘    └─
typ       └───┘└──┘└─
doc       └───┘    └─
txt       └───┘    └─
par       └───┘    └─
pid          └┘    
st       └────────┘
453  
src  
typ  
doc  
txt  
par  
pid  
st   
454  lemma closure_subtype {x : {a // p a}} {s : set {a // p a}}:
id                                           └─┘      
src                                             └─┘ 
typ                                          └─┘      
455    x ∈ closure s ↔ x.val ∈ closure (subtype.val '' s) :=
id       └─────┘   └──┘  └─────┘  └─────────┘ └┘ 
src       └─────┘     └──┘  └─────┘  └─────────┘ └┘
typ      └─────┘   └──┘  └─────┘  └─────────┘ └┘ 
doc        └─────┘             └─────┘
456  closure_induced $ assume x y, subtype.eq
id   └─────────────┘             └────────┘
src  └─────────────┘               └────────┘
typ  └─────────────┘             └────────┘
457  
458  end subtype
459  
460  section quotient
461  variables [topological_space α] [topological_space β] [topological_space γ]
id              └───────────────┘     └───────────────┘     └───────────────┘
src             └───────────────┘     └───────────────┘     └───────────────┘
typ             └───────────────┘     └───────────────┘     └───────────────┘
doc             └───────────────┘     └───────────────┘     └───────────────┘
462  variables {r : α → α → Prop} {s : setoid α}
id                                     └────┘
src                                    └────┘
typ                                    └────┘
463  
464  lemma quotient_map_quot_mk : quotient_map (@quot.mk α r) :=
id                                └──────────┘   └─────┘  
src                               └──────────┘
typ                               └──────────┘   └─────┘  
doc                               └──────────┘
465  ⟨quot.exists_rep, rfl⟩
id    └─────────────┘  └─┘
src   └─────────────┘  └─┘
typ   └─────────────┘  └─┘
466  
467  lemma continuous_quot_mk : continuous (@quot.mk α r) :=
id                              └────────┘   └─────┘  
src                             └────────┘
typ                             └────────┘   └─────┘  
doc                             └────────┘
468  continuous_coinduced_rng
id   └──────────────────────┘
src  └──────────────────────┘
typ  └──────────────────────┘
469  
470  lemma continuous_quot_lift {f : α → β} (hr : ∀ a b, r a b → f a = f b)
id                                                            
src                                                                  
typ                                                           
471    (h : continuous f) : continuous (quot.lift f hr : quot r → β) :=
id          └────────┘     └────────┘  └───────┘  └┘   └──┘    
src         └────────┘      └────────┘
typ         └────────┘     └────────┘  └───────┘  └┘   └──┘    
doc         └────────┘      └────────┘
472  continuous_coinduced_dom h
id   └──────────────────────┘ 
src  └──────────────────────┘
typ  └──────────────────────┘ 
473  
474  lemma quotient_map_quotient_mk : quotient_map (@quotient.mk α s) :=
id                                    └──────────┘   └─────────┘  
src                                   └──────────┘   └─────────┘
typ                                   └──────────┘   └─────────┘  
doc                                   └──────────┘
475  quotient_map_quot_mk
id   └──────────────────┘
src  └──────────────────┘
typ  └──────────────────┘
476  
477  lemma continuous_quotient_mk : continuous (@quotient.mk α s) :=
id                                  └────────┘   └─────────┘  
src                                 └────────┘   └─────────┘
typ                                 └────────┘   └─────────┘  
doc                                 └────────┘
478  continuous_coinduced_rng
id   └──────────────────────┘
src  └──────────────────────┘
typ  └──────────────────────┘
479  
480  lemma continuous_quotient_lift {f : α → β} (hs : ∀ a b, a ≈ b → f a = f b)
id                                                                
src                                                                     
typ                                                               
481    (h : continuous f) : continuous (quotient.lift f hs : quotient s → β) :=
id          └────────┘     └────────┘  └───────────┘  └┘   └──────┘    
src         └────────┘      └────────┘  └───────────┘        └──────┘
typ         └────────┘     └────────┘  └───────────┘  └┘   └──────┘    
doc         └────────┘      └────────┘
482  continuous_coinduced_dom h
id   └──────────────────────┘ 
src  └──────────────────────┘
typ  └──────────────────────┘ 
483  
484  end quotient
485  
486  section pi
487  variables {ι : Type*} {π : ι → Type*}
488  open topological_space
489  
490  lemma continuous_pi [topological_space α] [∀i, topological_space (π i)] {f : α → Πi:ι, π i}
id                        └───────────────┘       └───────────────┘                    
src                       └───────────────┘         └───────────────┘
typ                       └───────────────┘       └───────────────┘                    
doc                       └───────────────┘         └───────────────┘
491    (h : ∀i, continuous (λa, f a i)) : continuous f :=
id             └────────┘            └────────┘ 
src             └────────┘                └────────┘
typ            └────────┘            └────────┘ 
doc             └────────┘                └────────┘
492  continuous_infi_rng $ assume i, continuous_induced_rng $ h i
id   └─────────────────┘            └────────────────────┘    
src  └─────────────────┘             └────────────────────┘
typ  └─────────────────┘            └────────────────────┘    
493  
494  lemma continuous_apply [∀i, topological_space (π i)] (i : ι) :
id                              └───────────────┘           
src                              └───────────────┘
typ                             └───────────────┘           
doc                              └───────────────┘
495    continuous (λp:Πi, π i, p i) :=
id     └────────┘            
src    └────────┘
typ    └────────┘            
doc    └────────┘
496  continuous_infi_dom continuous_induced_dom
id   └─────────────────┘ └────────────────────┘
src  └─────────────────┘ └────────────────────┘
typ  └─────────────────┘ └────────────────────┘
497  
498  /-- Embedding a factor into a product space (by fixing arbitrarily all the other coordinates) is
499  continuous. -/
500  lemma continuous_update [decidable_eq ι] [∀i, topological_space (π i)] {i : ι} {f : Πi:ι, π i} :
id                            └──────────┘       └───────────────┘                        
src                           └──────────┘         └───────────────┘
typ                           └──────────┘       └───────────────┘                        
doc                                                └───────────────┘
501    continuous (λ x : π i, function.update f i x) :=
id     └────────┘           └─────────────┘   
src    └────────┘             └─────────────┘
typ    └────────┘           └─────────────┘   
doc    └────────┘             └─────────────┘
502  begin
st   └─────
503    refine continuous_pi (λj, _),
id            └───────────┘
src    └─────┘└───────────┘  └───┘
typ    └─────┘└───────────┘  └───┘
doc    └─────┘               └───┘
txt    └─────┘               └───┘
par    └─────┘               └───┘
pid                         └───┘
st   ─────────────────────────────┘└─
504    by_cases h : j = i,
id                    
src    └───────┘ └─┘ 
typ    └───────┘ └─┘
doc    └───────┘ └─┘  
txt    └───────┘ └─┘  
par    └───────┘ └─┘  
pid             └─┘  
st   ───────────────────┘└─
505    { rw h,
id          
src      └─┘
typ      └─┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───┘└──┘└─
506      simpa using continuous_id },
id                   └───────────┘
src      └──────────┘└───────────┘
typ      └──────────┘└───────────┘
doc      └──────────┘             
txt      └──────────┘             
par      └──────────┘             
pid           └────┘             
st   ─────────────────────────────┘└┘
507    { simpa [h] using continuous_const }
id                      └──────────────┘
src      └─────┘ └──────┘└──────────────┘
typ      └─────┘└──────┘└──────────────┘
doc      └─────┘ └──────┘                
txt      └─────┘ └──────┘                
par      └─────┘ └──────┘                
pid            └────┘                
st   ────────────────────────────────────┘└─
508  end
st   ──┘
509  
510  lemma nhds_pi [t : ∀i, topological_space (π i)] {a : Πi, π i} :
id                         └───────────────┘               
src                         └───────────────┘
typ                        └───────────────┘               
doc                         └───────────────┘
511    𝓝 a = (⨅i, comap (λx, x i) (𝓝 (a i))) :=
id          └───┘            
src           └───┘            
typ         └───┘            
doc            └───┘            
512  calc 𝓝 a = (⨅i, @nhds _ (@topological_space.induced _ _ (λx:Πi, π i, x i) (t i)) a) : nhds_infi
id               └──┘     └───────────────────────┘                           └───────┘
src                └──┘     └───────────────────────┘                                   └───────┘
typ              └──┘     └───────────────────────┘                           └───────┘
doc                └──┘     └───────────────────────┘
513    ... = (⨅i, comap (λx, x i) (𝓝 (a i))) : by simp [nhds_induced]
id             └───┘                           └──────────┘
src             └───┘                          └────┘└──────────┘└─
typ            └───┘                     └────┘└──────────┘└─
doc             └───┘                          └────┘            └─
txt                                               └────┘            └─
par                                               └────┘            └─
pid                                                               
st                                               └────────────────────
514  
src  
typ  
doc  
txt  
par  
pid  
st   
515  lemma is_open_set_pi [∀a, topological_space (π a)] {i : set ι} {s : Πa, set (π a)}
id                            └───────────────┘           └─┘           └─┘   
src                            └───────────────┘             └─┘             └─┘
typ                           └───────────────┘           └─┘           └─┘   
doc                            └───────────────┘
516    (hi : finite i) (hs : ∀a∈i, is_open (s a)) : is_open (pi i s) :=
id           └────┘             └─────┘        └─────┘  └┘  
src          └────┘               └─────┘          └─────┘  └┘
typ          └────┘             └─────┘        └─────┘  └┘  
doc          └────┘                └─────┘          └─────┘  └┘
517  by rw [pi_def]; exact (is_open_bInter hi $ assume a ha, continuous_apply a _ $ hs a ha)
id          └────┘          └────────────┘ └┘                └──────────────┘       └┘
src     └──┘└────┘  └────┘ └────────────┘         └─────┘└──────────────┘ └─┘      └─
typ     └──┘└────┘  └────┘ └────────────┘└┘       └─────┘└──────────────┘ └─┘ └┘   └─
doc     └──┘        └────┘                        └─────┘                 └─┘      └─
txt     └──┘        └────┘                        └─────┘                 └─┘      └─
par     └──┘        └────┘                        └─────┘                 └─┘      └─
pid       └┘                                     └─────┘                 └─┘      
st     └─────────┘└─────────────────────────────────────────────────────────────────────────
518  
src  
typ  
doc  
txt  
par  
pid  
st   
519  lemma pi_eq_generate_from [∀a, topological_space (π a)] :
id                                 └───────────────┘   
src                                 └───────────────┘
typ                                └───────────────┘   
doc                                 └───────────────┘
520    Pi.topological_space =
id     └──────────────────┘ 
src    └──────────────────┘ 
typ    └──────────────────┘ 
521    generate_from {g | ∃(s:Πa, set (π a)) (i : finset ι), (∀a∈i, is_open (s a)) ∧ g = pi ↑i s} :=
id     └───────────┘          └─┘           └────┘        └─────┘         └┘  
src    └───────────┘            └─┘             └────┘           └─────┘            └┘ 
typ    └───────────┘          └─┘           └────┘        └─────┘         └┘  
doc    └───────────┘                              └────┘            └─────┘              └┘
522  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
523    (le_generate_from $ assume g ⟨s, i, hi, eq⟩, eq.symm ▸ is_open_set_pi (finset.finite_to_set _) hi)
id      └──────────────┘                 └┘  └┘     └───┘  └────────────┘  └──────────────────┘
src     └──────────────┘                       └┘     └───┘  └────────────┘  └──────────────────┘
typ     └──────────────┘                 └┘  └┘     └───┘  └────────────┘  └──────────────────┘
524    (le_infi $ assume a s ⟨t, ht, s_eq⟩, generate_open.basic _ $
id      └─────┘                         └─────────────────┘
src     └─────┘                             └─────────────────┘
typ     └─────┘                         └─────────────────┘
525      ⟨function.update (λa, univ) a t, {a}, by simpa using ht, by ext f; simp [s_eq.symm, pi]⟩)
id        └─────────────┘     └──┘                        └┘                             └┘
src       └─────────────┘      └──┘              └──────────┘       └───┘  └────┘         └┘└┘
typ       └─────────────┘     └──┘            └──────────┘└┘     └───┘  └────┘└───────┘└┘└┘
doc       └─────────────┘                         └──────────┘       └───┘  └────┘         └┘└┘
txt                                               └──────────┘       └───┘  └────┘         └┘  
par                                               └──────────┘       └───┘  └────┘         └┘  
pid                                                    └────┘          └┘               └┘  
st                                               └─────────────┘    └──────────────────────────┘
526  
527  lemma pi_generate_from_eq {g : Πa, set (set (π a))} :
id                                     └─┘  └─┘   
src                                     └─┘  └─┘
typ                                    └─┘  └─┘   
528    @Pi.topological_space ι π (λa, generate_from (g a)) =
id      └──────────────────┘       └───────────┘      
src     └──────────────────┘          └───────────┘        
typ     └──────────────────┘       └───────────┘      
doc                                   └───────────┘
529    generate_from {t | ∃(s:Πa, set (π a)) (i : finset ι), (∀a∈i, s a ∈ g a) ∧ t = pi ↑i s} :=
id     └───────────┘          └─┘           └────┘                 └┘  
src    └───────────┘            └─┘             └────┘                         └┘ 
typ    └───────────┘          └─┘           └────┘                 └┘  
doc    └───────────┘                              └────┘                             └┘
530  let G := {t | ∃(s:Πa, set (π a)) (i : finset ι), (∀a∈i, s a ∈ g a) ∧ t = pi ↑i s} in
id                    └─┘           └────┘                 └┘  
src                      └─┘             └────┘                         └┘ 
typ                   └─┘           └────┘                 └┘  
doc                                        └────┘                             └┘
531  begin
st   └─────
532    rw [pi_eq_generate_from],
id         └─────────────────┘
src    └──┘└─────────────────┘
typ    └──┘└─────────────────┘
doc    └──┘                   
txt    └──┘                   
par    └──┘                   
pid      └┘                   
st   ────────────────────────┘└──
533    refine le_antisymm (generate_from_mono _) (le_generate_from _),
id            └─────────┘  └────────────────┘     └──────────────┘
src    └─────┘└─────────┘ └────────────────┘└──┘ └──────────────┘└─┘
typ    └─────┘└─────────┘ └────────────────┘└──┘ └──────────────┘└─┘
doc    └─────┘                              └──┘                 └─┘
txt    └─────┘                              └──┘                 └─┘
par    └─────┘                              └──┘                 └─┘
pid                                        └──┘                 └─┘
st   ───────────────────────────────────────────────────────────────┘└─
534    exact assume s ⟨t, i, ht, eq⟩, ⟨t, i, assume a ha, generate_open.basic _ (ht a ha), eq⟩,
id                         └┘  └┘                       └─────────────────┘
src    └────┘      └──┘ └┘ └┘  └┘└┘└─┘  └┘ └┘      └─────┘└─────────────────┘└─┘      └─┘  
typ    └────┘      └──┘└┘└┘└┘└┘└┘└─┘  └┘ └┘      └─────┘└─────────────────┘└─┘      └─┘  
doc    └────┘      └──┘ └┘ └┘  └┘  └─┘  └┘ └┘      └─────┘                   └─┘      └─┘  
txt    └────┘      └──┘ └┘ └┘  └┘  └─┘  └┘ └┘      └─────┘                   └─┘      └─┘  
par    └────┘      └──┘ └┘ └┘  └┘  └─┘  └┘ └┘      └─────┘                   └─┘      └─┘  
pid               └──┘ └┘ └┘  └┘  └─┘  └┘ └┘      └─────┘                   └─┘      └─┘  
st   ────────────────────────────────────────────────────────────────────────────────────────┘└─
535    { rintros s ⟨t, i, hi, rfl⟩,
src      └───────────────────────┘
typ      └───────────────────────┘
doc      └───────────────────────┘
txt      └───────────────────────┘
par      └───────────────────────┘
pid             └────────────────┘
st   ────────────────────────────┘└─
536      rw [pi_def],
id           └────┘
src      └──┘└────┘
typ      └──┘└────┘
doc      └──┘      
txt      └──┘      
par      └──┘      
pid        └┘      
st   ─────────────┘└──
537      apply is_open_bInter (finset.finite_to_set _),
id             └────────────┘  └──────────────────┘
src      └────┘└────────────┘ └──────────────────┘└─┘
typ      └────┘└────────────┘ └──────────────────┘└─┘
doc      └────┘                                   └─┘
txt      └────┘                                   └─┘
par      └────┘                                   └─┘
pid                                              └─┘
st   ────────────────────────────────────────────────┘└─
538      assume a ha, show ((generate_from G).coinduced (λf:Πa, π a, f a)).is_open (t a),
id                           └───────────┘                                         
src      └─────────┘  └───┘  └───────────┘ └──────────┘  └┘    └┘  └─────────┘   
typ      └─────────┘  └───┘  └───────────┘└──────────┘  └┘   └┘  └─────────┘ 
doc      └─────────┘  └───┘  └───────────┘ └──────────┘  └┘    └┘  └─────────┘   
txt      └─────────┘  └───┘                └──────────┘  └┘    └┘  └─────────┘   
par      └─────────┘  └───┘                └──────────┘  └┘    └┘  └─────────┘   
pid      └─────────┘  └───┘                └──────────┘  └┘    └┘  └─────────┘   
st   ──────────────┘└──────────────────────────────────────────────────────────────────┘└─
539      refine le_generate_from _ _ (hi a ha),
id              └──────────────┘      └┘  └┘
src      └─────┘└──────────────┘└───┘      
typ      └─────┘└──────────────┘└───┘ └┘└┘
doc      └─────┘                └───┘      
txt      └─────┘                └───┘      
par      └─────┘                └───┘      
pid                            └───┘      
st   ────────────────────────────────────────┘└─
540      exact assume s hs, generate_open.basic _ ⟨function.update (λa, univ) a s, {a}, by simp [hs]⟩ }
id                          └─────────────────┘    └─────────────┘      └──┘                    └┘
src      └────┘      └─────┘└─────────────────┘└─┘ └─────────────┘  └─┘└──┘└┘  └┘└──┘  └────┘  └┘
typ      └────┘      └─────┘└─────────────────┘└─┘ └─────────────┘  └─┘└──┘└┘  └┘└──┘  └────┘└┘└┘
doc      └────┘      └─────┘                   └─┘ └─────────────┘  └─┘    └┘  └┘ └──┘  └────┘  └┘
txt      └────┘      └─────┘                   └─┘                  └─┘    └┘  └┘ └──┘  └────┘  └┘
par      └────┘      └─────┘                   └─┘                  └─┘    └┘  └┘ └──┘  └────┘  └┘
pid                 └─────┘                   └─┘                  └─┘    └┘  └┘ └──┘  └─────┘  └┘
st   ────────────────────────────────────────────────────────────────────────────────────┘└────────┘└┘└─
541  end
st   ──┘
542  
543  lemma pi_generate_from_eq_fintype {g : Πa, set (set (π a))} [fintype ι] (hg : ∀a, ⋃₀ g a = univ) :
id                                             └─┘  └─┘        └─────┘            └┘    └──┘
src                                             └─┘  └─┘          └─────┘              └┘      └──┘
typ                                            └─┘  └─┘        └─────┘            └┘    └──┘
doc                                                               └─────┘
544    @Pi.topological_space ι π (λa, generate_from (g a)) =
id      └──────────────────┘       └───────────┘      
src     └──────────────────┘          └───────────┘        
typ     └──────────────────┘       └───────────┘      
doc                                   └───────────┘
545    generate_from {t | ∃(s:Πa, set (π a)), (∀a, s a ∈ g a) ∧ t = pi univ s} :=
id     └───────────┘          └─┘                   └┘ └──┘ 
src    └───────────┘            └─┘                           └┘ └──┘
typ    └───────────┘          └─┘                   └┘ └──┘ 
doc    └───────────┘                                                └┘
546  let G := {t | ∃(s:Πa, set (π a)), (∀a, s a ∈ g a) ∧ t = pi univ s} in
id                    └─┘                   └┘ └──┘ 
src                      └─┘                           └┘ └──┘
typ                   └─┘                   └┘ └──┘ 
doc                                                          └┘
547  begin
st   └─────
548    rw [pi_generate_from_eq],
id         └─────────────────┘
src    └──┘└─────────────────┘
typ    └──┘└─────────────────┘
doc    └──┘                   
txt    └──┘                   
par    └──┘                   
pid      └┘                   
st   ────────────────────────┘└──
549    refine le_antisymm (generate_from_mono _) (le_generate_from _),
id            └─────────┘  └────────────────┘     └──────────────┘
src    └─────┘└─────────┘ └────────────────┘└──┘ └──────────────┘└─┘
typ    └─────┘└─────────┘ └────────────────┘└──┘ └──────────────┘└─┘
doc    └─────┘                              └──┘                 └─┘
txt    └─────┘                              └──┘                 └─┘
par    └─────┘                              └──┘                 └─┘
pid                                        └──┘                 └─┘
st   ───────────────────────────────────────────────────────────────┘└─
550    exact assume s ⟨t, ht, eq⟩, ⟨t, finset.univ, by simp [ht, eq]⟩,
id                                    └─────────┘           └┘  └┘
src    └────┘      └──┘ └┘  └┘  └─┘  └┘└─────────┘└┘  └────┘  └┘└┘
typ    └────┘      └──┘└┘  └┘  └─┘  └┘└─────────┘└┘  └────┘└┘└┘└┘
doc    └────┘      └──┘ └┘  └┘  └─┘  └┘└─────────┘└┘  └────┘  └┘  
txt    └────┘      └──┘ └┘  └┘  └─┘  └┘           └┘  └────┘  └┘  
par    └────┘      └──┘ └┘  └┘  └─┘  └┘           └┘  └────┘  └┘  
pid               └──┘ └┘  └┘  └─┘  └┘           └┘  └─────┘  └┘  └┘
st   ────────────────────────────────────────────────┘└────────────┘└─
551    { rintros s ⟨t, i, ht, rfl⟩,
src      └───────────────────────┘
typ      └───────────────────────┘
doc      └───────────────────────┘
txt      └───────────────────────┘
par      └───────────────────────┘
pid             └────────────────┘
st   ────────────────────────────┘└─
552      apply is_open_iff_forall_mem_open.2 _,
id             └─────────────────────────┘
src      └────┘└─────────────────────────┘└──┘
typ      └────┘└─────────────────────────┘└──┘
doc      └────┘                           └──┘
txt      └────┘                           └──┘
par      └────┘                           └──┘
pid                                      └──┘
st   ────────────────────────────────────────┘└─
553      assume f hf,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ──────────────┘└─
554      choose c hc using show ∀a, ∃s, s ∈ g a ∧ f a ∈ s,
id                                            
src      └────────────────┘              └─
typ      └────────────────┘            └─
doc      └────────────────┘                 └─
txt      └────────────────┘                 └─
par      └────────────────┘                 └─
pid            └┘└─┘└─────┘                 └─
st   ──────────────────────────────────────────────────────
555      { assume a, have : f a ∈ ⋃₀ g a, { rw [hg], apply mem_univ }, simpa },
id                               └┘          └┘         └──────┘
src  ─────┘└──────┘└┘└─────┘   └┘  └──┘└──┘  └┘└────┘└──────┘└─┘└────┘
typ  ─────┘└──────┘└┘└─────┘  └┘└──┘└──┘└┘└┘└────┘└──────┘└─┘└────┘
doc  ─────┘└──────┘└┘└─────┘       └──┘└──┘  └┘└────┘        └─┘└────┘
txt  ─────┘└──────┘└┘└─────┘       └──┘└──┘  └┘└────┘        └─┘└────┘
par  ─────┘└──────┘└┘└─────┘       └──┘└──┘  └┘└────┘        └─┘└────┘
pid  ──────────────────────┘       └──────┘  └───────┘        └─────────┘
st   ────┘└───────┘└───────────────────┘└─┘└─────┘└────────────────┘└──────┘└┘
556      refine ⟨pi univ (λa, if a ∈ i then t a else (c : Πa, set (π a)) a), _, _, _⟩,
id               └┘ └──┘                                   └─┘  
src      └─────┘ └┘└──┘  └─┘  └─┘  └────┘  └────┘  └─┘  └─┘   └─┘ └─────────┘
typ      └─────┘ └┘└──┘  └─┘  └─┘ └────┘ └────┘ └─┘  └─┘  └─┘ └─────────┘
doc      └─────┘ └┘      └─┘  └─┘  └────┘  └────┘  └─┘        └─┘ └─────────┘
txt      └─────┘         └─┘  └─┘  └────┘  └────┘  └─┘        └─┘ └─────────┘
par      └─────┘         └─┘  └─┘  └────┘  └────┘  └─┘        └─┘ └─────────┘
pid                     └─┘  └─┘  └────┘  └────┘  └─┘        └─┘ └─────────┘
st   ───────────────────────────────────────────────────────────────────────────────┘└─
557      { simp [pi_if] },
id               └───┘
src        └────┘└───┘└┘
typ        └────┘└───┘└┘
doc        └────┘     └┘
txt        └────┘     └┘
par        └────┘     └┘
pid                 
st   ─────┘└───────────┘└┘
558      { refine generate_open.basic _ ⟨_, assume a, _, rfl⟩,
id                └─────────────────┘                    └─┘
src        └─────┘└─────────────────┘└─┘ └─┘      └─────┘└─┘
typ        └─────┘└─────────────────┘└─┘ └─┘      └─────┘└─┘
doc        └─────┘                   └─┘ └─┘      └─────┘   
txt        └─────┘                   └─┘ └─┘      └─────┘   
par        └─────┘                   └─┘ └─┘      └─────┘   
pid                                 └─┘ └─┘      └─────┘   
st   ─────┘└────────────────────────────────────────────────┘└─
559        by_cases a ∈ i; simp [*, pi] at * },
id                                └┘
src        └───────┘     └───────┘└┘└─────┘
typ        └───────┘   └───────┘└┘└─────┘
doc        └───────┘     └───────┘└┘└─────┘
txt        └───────┘     └───────┘  └─────┘
par        └───────┘     └───────┘  └─────┘
pid                         └──┘  └──┘
st   ───────────────────────────────────────┘└┘
560      { have : f ∈ pi {a | a ∉ i} c, { simp [*, pi] at * },
id                   └┘                        └┘
src        └─────┘  └┘└──┘   └┘     └───────┘└┘└─────┘
typ        └─────┘ └┘└──┘  └┘    └───────┘└┘└─────┘
doc        └─────┘  └┘ └──┘   └┘     └───────┘└┘└─────┘
txt        └─────┘     └──┘   └┘     └───────┘  └─────┘
par        └─────┘     └──┘   └┘     └───────┘  └─────┘
pid        └───┘└┘     └──┘   └┘         └──┘  └──┘
st   ────────────────────────────────┘└──┘└────────────────┘└┘
561        simpa [pi_if, hf] } }
id                └───┘  └┘
src        └─────┘└───┘└┘  └┘
typ        └─────┘└───┘└┘└┘└┘
doc        └─────┘     └┘  └┘
txt        └─────┘     └┘  └┘
par        └─────┘     └┘  └┘
pid                  └┘  
st   ───────────────────────┘└───
562  end
st   ──┘
563  
564  end pi
565  
566  section sigma
567  variables {ι : Type*} {σ : ι → Type*} [Π i, topological_space (σ i)]
id                                             └───────────────┘    
src                                              └───────────────┘
typ                                            └───────────────┘    
doc                                              └───────────────┘
568  open lattice
569  
570  lemma continuous_sigma_mk {i : ι} : continuous (@sigma.mk ι σ i) :=
id                                      └────────┘   └──────┘   
src                                      └────────┘   └──────┘
typ                                     └────────┘   └──────┘   
doc                                      └────────┘
571  continuous_supr_rng continuous_coinduced_rng
id   └─────────────────┘ └──────────────────────┘
src  └─────────────────┘ └──────────────────────┘
typ  └─────────────────┘ └──────────────────────┘
572  
573  lemma is_open_sigma_iff {s : set (sigma σ)} : is_open s ↔ ∀ i, is_open (sigma.mk i ⁻¹' s) :=
id                                └─┘  └───┘      └─────┘       └─────┘  └──────┘  └─┘ 
src                               └─┘  └───┘       └─────┘         └─────┘  └──────┘   └─┘
typ                               └─┘  └───┘      └─────┘       └─────┘  └──────┘  └─┘ 
doc                                                └─────┘          └─────┘             └─┘
574  by simp only [is_open_supr_iff, is_open_coinduced]
id                 └──────────────┘  └───────────────┘
src     └─────────┘└──────────────┘└┘└───────────────┘└─
typ     └─────────┘└──────────────┘└┘└───────────────┘└─
doc     └─────────┘                └┘                 └─
txt     └─────────┘                └┘                 └─
par     └─────────┘                └┘                 └─
pid         └──┘└┘                └┘                 
st     └────────────────────────────────────────────────
575  
src  
typ  
doc  
txt  
par  
pid  
st   
576  lemma is_closed_sigma_iff {s : set (sigma σ)} : is_closed s ↔ ∀ i, is_closed (sigma.mk i ⁻¹' s) :=
id                                  └─┘  └───┘      └───────┘       └───────┘  └──────┘  └─┘ 
src                                 └─┘  └───┘       └───────┘         └───────┘  └──────┘   └─┘
typ                                 └─┘  └───┘      └───────┘       └───────┘  └──────┘  └─┘ 
doc                                                  └───────┘          └───────┘             └─┘
577  is_open_sigma_iff
id   └───────────────┘
src  └───────────────┘
typ  └───────────────┘
578  
579  lemma is_open_map_sigma_mk {i : ι} : is_open_map (@sigma.mk ι σ i) :=
id                                       └─────────┘   └──────┘   
src                                       └─────────┘   └──────┘
typ                                      └─────────┘   └──────┘   
doc                                       └─────────┘
580  begin
st   └─────
581    intros s hs,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid          └───┘
st   ────────────┘└─
582    rw is_open_sigma_iff,
id        └───────────────┘
src    └─┘└───────────────┘
typ    └─┘└───────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ─────────────────────┘└─
583    intro j,
src    └─────┘
typ    └─────┘
doc    └─────┘
txt    └─────┘
par    └─────┘
pid         └┘
st   ────────┘└─
584    classical,
src    └───────┘
typ    └───────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
st   ──────────┘└─
585    by_cases h : i = j,
id                    
src    └───────┘ └─┘ 
typ    └───────┘ └─┘
doc    └───────┘ └─┘  
txt    └───────┘ └─┘  
par    └───────┘ └─┘  
pid             └─┘  
st   ───────────────────┘└─
586    { subst j,
id             
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└─────┘└─
587      convert hs,
id               └┘
src      └──────┘
typ      └──────┘└┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid             
st   ─────────────┘└─
588      exact set.preimage_image_eq _ injective_sigma_mk },
id             └───────────────────┘   └────────────────┘
src      └────┘└───────────────────┘└─┘└────────────────┘
typ      └────┘└───────────────────┘└─┘└────────────────┘
doc      └────┘                     └─┘                  
txt      └────┘                     └─┘                  
par      └────┘                     └─┘                  
pid                                └─┘                  
st   ────────────────────────────────────────────────────┘└┘
589    { convert is_open_empty,
id               └───────────┘
src      └──────┘└───────────┘
typ      └──────┘└───────────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid             
st   ────────────────────────┘└─
590      apply set.eq_empty_of_subset_empty,
id             └──────────────────────────┘
src      └────┘└──────────────────────────┘
typ      └────┘└──────────────────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ─────────────────────────────────────┘└─
591      rintro x ⟨y, _, hy⟩,
src      └─────────────────┘
typ      └─────────────────┘
doc      └─────────────────┘
txt      └─────────────────┘
par      └─────────────────┘
pid            └───────────┘
st   ──────────────────────┘└─
592      have : i = j, by cc,
id                 
src      └─────┘        └┘
typ      └─────┘      └┘
doc      └─────┘        └┘
txt      └─────┘        └┘
par      └─────┘        └┘
pid      └───┘└┘  
st   ───────────────┘       └─
593      contradiction }
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid                   
st   ─────────────────┘└─
594  end
st   ──┘
595  
596  lemma is_open_range_sigma_mk {i : ι} : is_open (set.range (@sigma.mk ι σ i)) :=
id                                         └─────┘  └───────┘   └──────┘   
src                                         └─────┘  └───────┘   └──────┘
typ                                        └─────┘  └───────┘   └──────┘   
doc                                         └─────┘  └───────┘
597  by { rw ←set.image_univ, exact is_open_map_sigma_mk _ is_open_univ }
id            └────────────┘        └──────────────────┘   └──────────┘
src       └──┘└────────────┘  └────┘└──────────────────┘└─┘└──────────┘
typ       └──┘└────────────┘  └────┘└──────────────────┘└─┘└──────────┘
doc       └──┘                └────┘                    └─┘            
txt       └──┘                └────┘                    └─┘            
par       └──┘                └────┘                    └─┘            
pid         └┘                                         └─┘            
st     └───────────────────┘└──────────────────────────────────────────┘└┘
598  
599  lemma is_closed_map_sigma_mk {i : ι} : is_closed_map (@sigma.mk ι σ i) :=
id                                         └───────────┘   └──────┘   
src                                         └───────────┘   └──────┘
typ                                        └───────────┘   └──────┘   
600  begin
st   └─────
601    intros s hs,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid          └───┘
st   ────────────┘└─
602    rw is_closed_sigma_iff,
id        └─────────────────┘
src    └─┘└─────────────────┘
typ    └─┘└─────────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ───────────────────────┘└─
603    intro j,
src    └─────┘
typ    └─────┘
doc    └─────┘
txt    └─────┘
par    └─────┘
pid         └┘
st   ────────┘└─
604    classical,
src    └───────┘
typ    └───────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
st   ──────────┘└─
605    by_cases h : i = j,
id                    
src    └───────┘ └─┘ 
typ    └───────┘ └─┘
doc    └───────┘ └─┘  
txt    └───────┘ └─┘  
par    └───────┘ └─┘  
pid             └─┘  
st   ───────────────────┘└─
606    { subst j,
id             
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└─────┘└─
607      convert hs,
id               └┘
src      └──────┘
typ      └──────┘└┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid             
st   ─────────────┘└─
608      exact set.preimage_image_eq _ injective_sigma_mk },
id             └───────────────────┘   └────────────────┘
src      └────┘└───────────────────┘└─┘└────────────────┘
typ      └────┘└───────────────────┘└─┘└────────────────┘
doc      └────┘                     └─┘                  
txt      └────┘                     └─┘                  
par      └────┘                     └─┘                  
pid                                └─┘                  
st   ────────────────────────────────────────────────────┘└┘
609    { convert is_closed_empty,
id               └─────────────┘
src      └──────┘└─────────────┘
typ      └──────┘└─────────────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid             
st   ──────────────────────────┘└─
610      apply set.eq_empty_of_subset_empty,
id             └──────────────────────────┘
src      └────┘└──────────────────────────┘
typ      └────┘└──────────────────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ─────────────────────────────────────┘└─
611      rintro x ⟨y, _, hy⟩,
src      └─────────────────┘
typ      └─────────────────┘
doc      └─────────────────┘
txt      └─────────────────┘
par      └─────────────────┘
pid            └───────────┘
st   ──────────────────────┘└─
612      have : i = j, by cc,
id                 
src      └─────┘        └┘
typ      └─────┘      └┘
doc      └─────┘        └┘
txt      └─────┘        └┘
par      └─────┘        └┘
pid      └───┘└┘  
st   ───────────────┘       └─
613      contradiction }
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid                   
st   ─────────────────┘└─
614  end
st   ──┘
615  
616  lemma is_closed_sigma_mk {i : ι} : is_closed (set.range (@sigma.mk ι σ i)) :=
id                                     └───────┘  └───────┘   └──────┘   
src                                     └───────┘  └───────┘   └──────┘
typ                                    └───────┘  └───────┘   └──────┘   
doc                                     └───────┘  └───────┘
617  by { rw ←set.image_univ, exact is_closed_map_sigma_mk _ is_closed_univ }
id            └────────────┘        └────────────────────┘   └────────────┘
src       └──┘└────────────┘  └────┘└────────────────────┘└─┘└────────────┘
typ       └──┘└────────────┘  └────┘└────────────────────┘└─┘└────────────┘
doc       └──┘                └────┘                      └─┘              
txt       └──┘                └────┘                      └─┘              
par       └──┘                └────┘                      └─┘              
pid         └┘                                           └─┘              
st     └───────────────────┘└──────────────────────────────────────────────┘└┘
618  
619  lemma open_embedding_sigma_mk {i : ι} : open_embedding (@sigma.mk ι σ i) :=
id                                          └────────────┘   └──────┘   
src                                          └────────────┘   └──────┘
typ                                         └────────────┘   └──────┘   
doc                                          └────────────┘
620  open_embedding_of_continuous_injective_open
id   └─────────────────────────────────────────┘
src  └─────────────────────────────────────────┘
typ  └─────────────────────────────────────────┘
621    continuous_sigma_mk injective_sigma_mk is_open_map_sigma_mk
id     └─────────────────┘ └────────────────┘ └──────────────────┘
src    └─────────────────┘ └────────────────┘ └──────────────────┘
typ    └─────────────────┘ └────────────────┘ └──────────────────┘
622  
623  lemma closed_embedding_sigma_mk {i : ι} : closed_embedding (@sigma.mk ι σ i) :=
id                                            └──────────────┘   └──────┘   
src                                            └──────────────┘   └──────┘
typ                                           └──────────────┘   └──────┘   
doc                                            └──────────────┘
624  closed_embedding_of_continuous_injective_closed
id   └─────────────────────────────────────────────┘
src  └─────────────────────────────────────────────┘
typ  └─────────────────────────────────────────────┘
625    continuous_sigma_mk injective_sigma_mk is_closed_map_sigma_mk
id     └─────────────────┘ └────────────────┘ └────────────────────┘
src    └─────────────────┘ └────────────────┘ └────────────────────┘
typ    └─────────────────┘ └────────────────┘ └────────────────────┘
626  
627  lemma embedding_sigma_mk {i : ι} : embedding (@sigma.mk ι σ i) :=
id                                     └───────┘   └──────┘   
src                                     └───────┘   └──────┘
typ                                    └───────┘   └──────┘   
doc                                     └───────┘
628  closed_embedding_sigma_mk.1
id   └───────────────────────┘
src  └───────────────────────┘
typ  └───────────────────────┘
629  
630  /-- A map out of a sum type is continuous if its restriction to each summand is. -/
631  lemma continuous_sigma [topological_space β] {f : sigma σ → β}
id                           └───────────────┘        └───┘    
src                          └───────────────┘         └───┘
typ                          └───────────────┘        └───┘    
doc                          └───────────────┘
632    (h : ∀ i, continuous (λ a, f ⟨i, a⟩)) : continuous f :=
id              └────────┘                └────────┘ 
src              └────────┘                    └────────┘
typ             └────────┘                └────────┘ 
doc              └────────┘                    └────────┘
633  continuous_supr_dom (λ i, continuous_coinduced_dom (h i))
id   └─────────────────┘      └──────────────────────┘   
src  └─────────────────┘       └──────────────────────┘
typ  └─────────────────┘      └──────────────────────┘   
634  
635  lemma continuous_sigma_map {κ : Type*} {τ : κ → Type*} [Π k, topological_space (τ k)]
id                                                              └───────────────┘   
src                                                               └───────────────┘
typ                                                             └───────────────┘   
doc                                                               └───────────────┘
636    {f₁ : ι → κ} {f₂ : Π i, σ i → τ (f₁ i)} (hf : ∀ i, continuous (f₂ i)) :
id                                └┘              └────────┘  └┘ 
src                                                       └────────┘
typ                               └┘              └────────┘  └┘ 
doc                                                       └────────┘
637    continuous (sigma.map f₁ f₂) :=
id     └────────┘  └───────┘ └┘ └┘
src    └────────┘  └───────┘
typ    └────────┘  └───────┘ └┘ └┘
doc    └────────┘  └───────┘
638  continuous_sigma $ λ i,
id   └──────────────┘     
src  └──────────────┘
typ  └──────────────┘     
doc  └──────────────┘
639    show continuous (λ a, sigma.mk (f₁ i) (f₂ i a)),
id          └────────┘      └──────┘  └┘    └┘  
src         └────────┘       └──────┘
typ         └────────┘      └──────┘  └┘    └┘  
doc         └────────┘
640    from continuous_sigma_mk.comp (hf i)
id          └─────────────────┘└───┘  └┘ 
src         └─────────────────┘└───┘
typ         └─────────────────┘└───┘  └┘ 
641  
642  lemma is_open_map_sigma [topological_space β] {f : sigma σ → β}
id                            └───────────────┘        └───┘    
src                           └───────────────┘         └───┘
typ                           └───────────────┘        └───┘    
doc                           └───────────────┘
643    (h : ∀ i, is_open_map (λ a, f ⟨i, a⟩)) : is_open_map f :=
id              └─────────┘                └─────────┘ 
src              └─────────┘                    └─────────┘
typ             └─────────┘                └─────────┘ 
doc              └─────────┘                    └─────────┘
644  begin
st   └─────
645    intros s hs,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid          └───┘
st   ────────────┘└─
646    rw is_open_sigma_iff at hs,
id        └───────────────┘
src    └─┘└───────────────┘└────┘
typ    └─┘└───────────────┘└────┘
doc    └─┘                 └────┘
txt    └─┘                 └────┘
par    └─┘                 └────┘
pid                       └────┘
st   ───────────────────────────┘└─
647    have : s = ⋃ i, sigma.mk i '' (sigma.mk i ⁻¹' s),
id                             └┘  └──────┘   └─┘ 
src    └─────┘ └┘         └┘ └──────┘ └─┘ 
typ    └─────┘ └┘         └┘ └──────┘ └─┘
doc    └─────┘  └┘                     └─┘ 
txt    └─────┘   └┘                          
par    └─────┘   └┘                          
pid    └───┘└┘   └┘                          
st   ─────────────────────────────────────────────────┘└─
648    { rw Union_image_preimage_sigma_mk_eq_self },
id          └───────────────────────────────────┘
src      └─┘└───────────────────────────────────┘
typ      └─┘└───────────────────────────────────┘
doc      └─┘                                     
txt      └─┘                                     
par      └─┘                                     
pid                                             
st   ───┘└───────────────────────────────────────┘└┘
649    rw this,
id        └──┘
src    └─┘
typ    └─┘└──┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────┘└─
650    rw [image_Union],
id         └─────────┘
src    └──┘└─────────┘
typ    └──┘└─────────┘
doc    └──┘           
txt    └──┘           
par    └──┘           
pid      └┘           
st   ────────────────┘└──
651    apply is_open_Union,
id           └───────────┘
src    └────┘└───────────┘
typ    └────┘└───────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ────────────────────┘└─
652    intro i,
src    └─────┘
typ    └─────┘
doc    └─────┘
txt    └─────┘
par    └─────┘
pid         └┘
st   ────────┘└─
653    rw [image_image],
id         └─────────┘
src    └──┘└─────────┘
typ    └──┘└─────────┘
doc    └──┘└─────────┘
txt    └──┘           
par    └──┘           
pid      └┘           
st   ────────────────┘└──
654    exact h i _ (hs i)
id                 └┘ 
src    └────┘  └─┘    └┘
typ    └────┘ └─┘ └┘└┘
doc    └────┘  └─┘    └┘
txt    └────┘  └─┘    └┘
par    └────┘  └─┘    └┘
pid           └─┘    
st   ────────────────────┘
655  end
st   └─┘
656  
657  /-- The sum of embeddings is an embedding. -/
658  lemma embedding_sigma_map {τ : ι → Type*} [Π i, topological_space (τ i)]
id                                                 └───────────────┘   
src                                                  └───────────────┘
typ                                                └───────────────┘   
doc                                                  └───────────────┘
659    {f : Π i, σ i → τ i} (hf : ∀ i, embedding (f i)) : embedding (sigma.map id f) :=
id                               └───────┘        └───────┘  └───────┘ └┘ 
src                                    └───────┘          └───────┘  └───────┘ └┘
typ                              └───────┘        └───────┘  └───────┘ └┘ 
doc                                    └───────┘          └───────┘  └───────┘
660  begin
st   └─────
661    refine ⟨⟨_⟩, injective_sigma_map function.injective_id (λ i, (hf i).inj)⟩,
id                  └─────────────────┘ └───────────────────┘        └┘
src    └─────┘  └──┘└─────────────────┘└───────────────────┘  └──┘    └─────┘
typ    └─────┘  └──┘└─────────────────┘└───────────────────┘  └──┘ └┘ └─────┘
doc    └─────┘  └──┘                                          └──┘    └─────┘
txt    └─────┘  └──┘                                          └──┘    └─────┘
par    └─────┘  └──┘                                          └──┘    └─────┘
pid            └──┘                                          └──┘    └─────┘
st   ──────────────────────────────────────────────────────────────────────────┘└─
662    refine le_antisymm
id            └─────────┘
src    └─────┘└─────────┘
typ    └─────┘└─────────┘
doc    └─────┘           
txt    └─────┘           
par    └─────┘           
pid                     
st   ─────────────────────
663      (continuous_iff_le_induced.mp (continuous_sigma_map (λ i, (hf i).continuous))) _,
id        └──────────────────────────┘  └──────────────────┘        └┘
src  ───┘ └──────────────────────────┘ └──────────────────┘  └──┘    └───────────────┘
typ  ───┘ └──────────────────────────┘ └──────────────────┘  └──┘ └┘ └───────────────┘
doc  ───┘                                                    └──┘    └───────────────┘
txt  ───┘                                                    └──┘    └───────────────┘
par  ───┘                                                    └──┘    └───────────────┘
pid  ───┘                                                    └──┘    └───────────────┘
st   ───────────────────────────────────────────────────────────────────────────────────┘└─
664    intros s hs,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid          └───┘
st   ────────────┘└─
665    replace hs := is_open_sigma_iff.mp hs,
id                   └──────────────────┘ └┘
src    └────────────┘└──────────────────┘
typ    └────────────┘└──────────────────┘└┘
doc    └────────────┘                    
txt    └────────────┘                    
par    └────────────┘                    
pid           └─┘└─┘                    
st   ──────────────────────────────────────┘└─
666    have : ∀ i, ∃ t, is_open t ∧ f i ⁻¹' t = sigma.mk i ⁻¹' s,
id                    └─────┘        └─┘    └──────┘       
src    └─────┘ └┘ └┘└─────┘    └─┘ └──────┘    
typ    └─────┘ └┘ └┘└─────┘   └─┘ └──────┘    
doc    └─────┘ └┘  └┘ └─────┘    └─┘              
txt    └─────┘ └┘  └┘                             
par    └─────┘ └┘  └┘                             
pid    └───┘└┘ └┘  └┘                             
st   ──────────────────────────────────────────────────────────┘└─
667    { intro i,
src      └─────┘
typ      └─────┘
doc      └─────┘
txt      └─────┘
par      └─────┘
pid           └┘
st   ───┘└─────┘└─
668      apply is_open_induced_iff.mp,
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────────────────────────┘└─
669      convert hs i,
id               └┘ 
src      └──────┘  
typ      └──────┘└┘
doc      └──────┘  
txt      └──────┘  
par      └──────┘  
pid               
st   ───────────────┘└─
670      exact (hf i).induced.symm },
id              └┘ 
src      └────┘    └─────────────┘
typ      └────┘ └┘└─────────────┘
doc      └────┘    └─────────────┘
txt      └────┘    └─────────────┘
par      └────┘    └─────────────┘
pid               └───────────┘└┘
st   ─────────────────────────────┘└┘
671    choose t ht using this,
id                       └──┘
src    └────────────────┘
typ    └────────────────┘└──┘
doc    └────────────────┘
txt    └────────────────┘
par    └────────────────┘
pid          └┘└─┘└─────┘
st   ───────────────────────┘└─
672    apply is_open_induced_iff.mpr,
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ──────────────────────────────┘└─
673    refine ⟨⋃ i, sigma.mk i '' t i, is_open_Union (λ i, is_open_map_sigma_mk _ (ht i).1), _⟩,
id                └──────┘   └┘     └───────────┘       └──────────────────┘    └┘
src    └─────┘ └┘└──────┘ └┘  └┘└───────────┘  └──┘└──────────────────┘└─┘    └──────┘
typ    └─────┘ └┘└──────┘ └┘ └┘└───────────┘  └──┘└──────────────────┘└─┘ └┘ └──────┘
doc    └─────┘ └┘             └┘               └──┘                    └─┘    └──────┘
txt    └─────┘  └┘              └┘               └──┘                    └─┘    └──────┘
par    └─────┘  └┘              └┘               └──┘                    └─┘    └──────┘
pid            └┘              └┘               └──┘                    └─┘    └──────┘
st   ─────────────────────────────────────────────────────────────────────────────────────────┘└─
674    ext p,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid       └┘
st   ──────┘└─
675    rcases p with ⟨i, x⟩,
id            
src    └─────┘ └──────────┘
typ    └─────┘└──────────┘
doc    └─────┘ └──────────┘
txt    └─────┘ └──────────┘
par    └─────┘ └──────────┘
pid           └──────────┘
st   ─────────────────────┘└─
676    change (sigma.mk i (f i x) ∈ ⋃ (i : ι), sigma.mk i '' t i) ↔ x ∈ sigma.mk i ⁻¹' s,
id                                                               └──────┘      
src    └─────┘              └┘└────┘              └┘   └──────┘    
typ    └─────┘             └┘└────┘            └┘  └──────┘   
doc    └─────┘              └┘ └────┘              └┘               
txt    └─────┘              └┘  └────┘               └┘               
par    └─────┘              └┘  └────┘               └┘               
pid                        └┘  └────┘               └┘               
st   ──────────────────────────────────────────────────────────────────────────────────┘└─
677    rw [←(ht i).2, mem_Union],
id           └┘      └───────┘
src    └───┘    └───┘└───────┘
typ    └───┘ └┘└───┘└───────┘
doc    └───┘    └───┘         
txt    └───┘    └───┘         
par    └───┘    └───┘         
pid      └─┘    └───┘         
st   ────────────┘└───────────┘└──
678    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
679    { rintro ⟨j, hj⟩,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid            └──────┘
st   ───┘└────────────┘└─
680      rw mem_image at hj,
id          └───────┘
src      └─┘└───────┘└────┘
typ      └─┘└───────┘└────┘
doc      └─┘         └────┘
txt      └─┘         └────┘
par      └─┘         └────┘
pid                 └────┘
st   ─────────────────────┘└─
681      rcases hj with ⟨y, hy₁, hy₂⟩,
id              └┘
src      └─────┘  └─────────────────┘
typ      └─────┘└┘└─────────────────┘
doc      └─────┘  └─────────────────┘
txt      └─────┘  └─────────────────┘
par      └─────┘  └─────────────────┘
pid              └─────────────────┘
st   ───────────────────────────────┘└─
682      rcases sigma.mk.inj_iff.mp hy₂ with ⟨rfl, hy⟩,
id              └─────────────────┘ └─┘
src      └─────┘└─────────────────┘   └─────────────┘
typ      └─────┘└─────────────────┘└─┘└─────────────┘
doc      └─────┘                      └─────────────┘
txt      └─────┘                      └─────────────┘
par      └─────┘                      └─────────────┘
pid                                  └─────────────┘
st   ────────────────────────────────────────────────┘└─
683      replace hy := eq_of_heq hy,
id                     └───────┘ └┘
src      └────────────┘└───────┘
typ      └────────────┘└───────┘└┘
doc      └────────────┘         
txt      └────────────┘         
par      └────────────┘         
pid             └─┘└─┘         
st   ─────────────────────────────┘└─
684      subst y,
id             
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ──────────┘└─
685      exact hy₁ },
id             └─┘
src      └────┘   
typ      └────┘└─┘
doc      └────┘   
txt      └────┘   
par      └────┘   
pid              
st   ─────────────┘└┘
686    { intro hx,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid           └─┘
st   ───────────┘└─
687      use i,
id           
src      └──┘
typ      └──┘
doc      └──┘
txt      └──┘
par      └──┘
pid         
st   ────────┘└─
688      rw mem_image,
id          └───────┘
src      └─┘└───────┘
typ      └─┘└───────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───────────────┘└─
689      exact ⟨f i x, hx, rfl⟩ }
id                  └┘  └─┘
src      └────┘    └┘  └┘└─┘└┘
typ      └────┘ └┘└┘└┘└─┘└┘
doc      └────┘    └┘  └┘   └┘
txt      └────┘    └┘  └┘   └┘
par      └────┘    └┘  └┘   └┘
pid               └┘  └┘   
st   ──────────────────────────┘└─
690  end
st   ──┘
691  
692  end sigma
693  
694  lemma mem_closure_of_continuous [topological_space α] [topological_space β]
id                                    └───────────────┘    └───────────────┘ 
src                                   └───────────────┘     └───────────────┘
typ                                   └───────────────┘    └───────────────┘ 
doc                                   └───────────────┘     └───────────────┘
695    {f : α → β} {a : α} {s : set α} {t : set β}
id                           └─┘        └─┘ 
src                             └─┘         └─┘
typ                          └─┘        └─┘ 
696    (hf : continuous f) (ha : a ∈ closure s) (h : ∀a∈s, f a ∈ closure t) :
id           └────────┘           └─────┘               └─────┘ 
src          └────────┘             └─────┘                    └─────┘
typ          └────────┘           └─────┘               └─────┘ 
doc          └────────┘              └─────┘                     └─────┘
697    f a ∈ closure t :=
id        └─────┘ 
src         └─────┘
typ       └─────┘ 
doc          └─────┘
698  calc f a ∈ f '' closure s : mem_image_of_mem _ ha
id             └┘ └─────┘    └──────────────┘   └┘
src               └┘ └─────┘     └──────────────┘
typ            └┘ └─────┘    └──────────────┘   └┘
doc                  └─────┘
699    ... ⊆ closure (f '' s) : image_closure_subset_closure_image hf
id           └─────┘   └┘     └────────────────────────────────┘ └┘
src          └─────┘    └┘      └────────────────────────────────┘
typ          └─────┘   └┘     └────────────────────────────────┘ └┘
doc          └─────┘
700    ... ⊆ closure (closure t) : closure_mono $ image_subset_iff.mpr $ h
id           └─────┘  └─────┘     └──────────┘   └──────────────┘└──┘   
src          └─────┘  └─────┘      └──────────┘   └──────────────┘└──┘
typ          └─────┘  └─────┘     └──────────┘   └──────────────┘└──┘   
doc          └─────┘  └─────┘                     └──────────────┘
701    ... ⊆ closure t : begin rw [closure_eq_of_is_closed], exact subset.refl _, exact is_closed_closure end
id           └─────┘              └─────────────────────┘         └─────────┘          └───────────────┘
src          └─────┘           └──┘└─────────────────────┘  └────┘└─────────┘└┘  └────┘└───────────────┘
typ          └─────┘          └──┘└─────────────────────┘  └────┘└─────────┘└┘  └────┘└───────────────┘
doc          └─────┘           └──┘                         └────┘           └┘  └────┘                 
txt                            └──┘                         └────┘           └┘  └────┘                 
par                            └──┘                         └────┘           └┘  └────┘                 
pid                              └┘                                         └┘                        
st                       └───────────────────────────────┘└────────────────────┘└────────────────────────┘└─┘
702  
703  lemma mem_closure_of_continuous2 [topological_space α] [topological_space β] [topological_space γ]
id                                     └───────────────┘    └───────────────┘    └───────────────┘ 
src                                    └───────────────┘     └───────────────┘     └───────────────┘
typ                                    └───────────────┘    └───────────────┘    └───────────────┘ 
doc                                    └───────────────┘     └───────────────┘     └───────────────┘
704    {f : α → β → γ} {a : α} {b : β} {s : set α} {t : set β} {u : set γ}
id                                     └─┘        └─┘        └─┘ 
src                                         └─┘         └─┘         └─┘
typ                                    └─┘        └─┘        └─┘ 
705    (hf : continuous (λp:α×β, f p.1 p.2)) (ha : a ∈ closure s) (hb : b ∈ closure t)
id           └────────┘                      └─────┘           └─────┘ 
src          └────────┘                            └─────┘             └─────┘
typ          └────────┘                      └─────┘           └─────┘ 
doc          └────────┘                                └─────┘              └─────┘
706    (h : ∀a∈s, ∀b∈t, f a b ∈ closure u) :
id                      └─────┘ 
src                            └─────┘
typ                     └─────┘ 
doc                             └─────┘
707    f a b ∈ closure u :=
id         └─────┘ 
src           └─────┘
typ        └─────┘ 
doc            └─────┘
708  have (a,b) ∈ closure (set.prod s t),
id            └─────┘  └──────┘  
src             └─────┘  └──────┘
typ           └─────┘  └──────┘  
doc               └─────┘  └──────┘
709    by simp [closure_prod_eq, ha, hb],
id              └─────────────┘  └┘  └┘
src       └────┘└─────────────┘└┘  └┘  
typ       └────┘└─────────────┘└┘└┘└┘└┘
doc       └────┘               └┘  └┘  
txt       └────┘               └┘  └┘  
par       └────┘               └┘  └┘  
pid                          └┘  └┘  
st       └─────────────────────────────┘
710  show f (a, b).1 (a, b).2 ∈ closure u,
id                    └─────┘ 
src                        └─────┘
typ                   └─────┘ 
doc                             └─────┘
711    from @mem_closure_of_continuous (α×β) _ _ _ (λp:α×β, f p.1 p.2) (a,b) _ u hf this $
id           └───────────────────────┘                            └┘ └──┘
src          └───────────────────────┘                             
typ          └───────────────────────┘                            └┘ └──┘
712      assume ⟨p₁, p₂⟩ ⟨h₁, h₂⟩, h p₁ h₁ p₂ h₂
id              └┘  └┘  └┘  └┘   
typ             └┘  └┘  └┘  └┘